Nuprl Lemma : qmax-symmetry

[x,y:ℚ].  (qmax(x;y) qmax(y;x) ∈ ℚ)


Proof




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

Latex:
\mforall{}[x,y:\mBbbQ{}].    (qmax(x;y)  =  qmax(y;x))



Date html generated: 2018_05_21-PM-11_57_22
Last ObjectModification: 2017_07_26-PM-06_47_33

Theory : rationals


Home Index