Nuprl Lemma : qmax_lb

[a,b,c:ℚ].  uiff(qmax(b;c) ≤ a;(b ≤ a) ∧ (c ≤ a))


Proof




Definitions occuring in Statement :  qmax: qmax(x;y) qle: r ≤ s rationals: uiff: uiff(P;Q) uall: [x:A]. B[x] and: P ∧ Q
Definitions unfolded in proof :  qmax: qmax(x;y) member: t ∈ T uall: [x:A]. B[x] uiff: uiff(P;Q) and: P ∧ Q uimplies: supposing a guard: {T} implies:  Q prop: true: True all: x:A. B[x] bool: 𝔹 unit: Unit it: btrue: tt ifthenelse: if then else fi  bfalse: ff squash: T
Lemmas referenced :  q_le_wf bool_wf equal-wf-T-base assert_wf qle_wf qle_transitivity_qorder qle_witness bnot_wf not_wf qle_complement_qorder qless_transitivity_2_qorder qle_weakening_lt_qorder qmax_wf rationals_wf uiff_transitivity2 eqtt_to_assert assert-q_le-eq uiff_transitivity eqff_to_assert assert_of_bnot squash_wf true_wf equal_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis equalityTransitivity equalitySymmetry baseClosed because_Cache independent_pairFormation isect_memberFormation independent_isectElimination sqequalRule productElimination independent_pairEquality independent_functionElimination productEquality natural_numberEquality isect_memberEquality lambdaFormation unionElimination equalityElimination applyEquality lambdaEquality imageElimination universeEquality imageMemberEquality dependent_functionElimination

Latex:
\mforall{}[a,b,c:\mBbbQ{}].    uiff(qmax(b;c)  \mleq{}  a;(b  \mleq{}  a)  \mwedge{}  (c  \mleq{}  a))



Date html generated: 2018_05_21-PM-11_55_13
Last ObjectModification: 2017_07_26-PM-06_46_03

Theory : rationals


Home Index