Nuprl Lemma : qmax-eq-iff-1

[q,r:ℚ].  uiff(qmax(q;r) q ∈ ℚ;r ≤ q)


Proof




Definitions occuring in Statement :  qmax: qmax(x;y) qle: r ≤ s rationals: uiff: uiff(P;Q) uall: [x:A]. B[x] equal: t ∈ T
Definitions unfolded in proof :  rev_implies:  Q not: ¬A false: False assert: b bnot: ¬bb sq_type: SQType(T) or: P ∨ Q exists: x:A. B[x] bfalse: ff ifthenelse: if then else fi  iff: ⇐⇒ Q guard: {T} prop: uimplies: supposing a and: P ∧ Q uiff: uiff(P;Q) btrue: tt it: unit: Unit bool: 𝔹 implies:  Q all: x:A. B[x] qmax: qmax(x;y) member: t ∈ T uall: [x:A]. B[x]
Lemmas referenced :  rationals_wf qle_weakening_lt_qorder qless_trichot_qorder assert-bnot bool_subtype_base bool_wf subtype_base_sq bool_cases_sqequal eqff_to_assert qle_wf qle_antisymmetry qle_witness qle_weakening_eq_qorder iff_weakening_equal assert-q_le-eq eqtt_to_assert q_le_wf
Rules used in proof :  axiomEquality isectIsTypeImplies isect_memberEquality_alt independent_pairEquality voidElimination because_Cache cumulativity instantiate dependent_functionElimination promote_hyp dependent_pairFormation_alt universeIsType equalityIstype independent_pairFormation sqequalRule independent_functionElimination independent_isectElimination productElimination equalitySymmetry equalityTransitivity equalityElimination unionElimination lambdaFormation_alt inhabitedIsType hypothesis hypothesisEquality thin isectElimination sqequalHypSubstitution extract_by_obid cut introduction isect_memberFormation_alt sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}[q,r:\mBbbQ{}].    uiff(qmax(q;r)  =  q;r  \mleq{}  q)



Date html generated: 2019_10_29-AM-07_43_57
Last ObjectModification: 2019_10_21-PM-06_08_23

Theory : rationals


Home Index