Nuprl Lemma : qmax_strict_lb

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


Proof




Definitions occuring in Statement :  qmax: qmax(x;y) qless: 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 qless_transitivity_1_qorder qless_witness qless_wf bnot_wf not_wf qle_complement_qorder qless_transitivity 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)  <  a;b  <  a  \mwedge{}  c  <  a)



Date html generated: 2018_05_21-PM-11_55_32
Last ObjectModification: 2017_07_26-PM-06_46_16

Theory : rationals


Home Index