Nuprl Lemma : qmax_strict_ub

a,b,c:ℚ.  (a < qmax(b;c) ⇐⇒ a < b ∨ a < c)


Proof




Definitions occuring in Statement :  qmax: qmax(x;y) qless: r < s rationals: all: x:A. B[x] iff: ⇐⇒ Q or: P ∨ Q
Definitions unfolded in proof :  all: x:A. B[x] qmax: qmax(x;y) member: t ∈ T uall: [x:A]. B[x] iff: ⇐⇒ Q and: P ∧ Q implies:  Q guard: {T} or: P ∨ Q prop: rev_implies:  Q uimplies: supposing a true: True uiff: uiff(P;Q) bool: 𝔹 unit: Unit it: btrue: tt ifthenelse: if then else fi  bfalse: ff squash: T
Lemmas referenced :  rationals_wf q_le_wf bool_wf equal-wf-T-base assert_wf qle_wf qless_wf qless_transitivity_2_qorder or_wf bnot_wf not_wf qle_complement_qorder qless_transitivity 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 lambdaFormation cut introduction extract_by_obid hypothesis sqequalHypSubstitution isectElimination thin hypothesisEquality equalityTransitivity equalitySymmetry baseClosed because_Cache independent_pairFormation sqequalRule inrFormation unionElimination independent_isectElimination natural_numberEquality inlFormation productElimination equalityElimination independent_functionElimination applyEquality lambdaEquality imageElimination universeEquality imageMemberEquality dependent_functionElimination

Latex:
\mforall{}a,b,c:\mBbbQ{}.    (a  <  qmax(b;c)  \mLeftarrow{}{}\mRightarrow{}  a  <  b  \mvee{}  a  <  c)



Date html generated: 2018_05_21-PM-11_55_04
Last ObjectModification: 2017_07_26-PM-06_45_57

Theory : rationals


Home Index