Nuprl Lemma : qmax_ub

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


Proof




Definitions occuring in Statement :  qmax: qmax(x;y) qle: 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 bool: 𝔹 unit: Unit it: btrue: tt uiff: uiff(P;Q) 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 qle_transitivity_qorder or_wf 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_1_qorder qle_weakening_lt_qorder
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 equalityElimination independent_functionElimination productElimination applyEquality lambdaEquality imageElimination universeEquality imageMemberEquality dependent_functionElimination

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



Date html generated: 2018_05_21-PM-11_54_55
Last ObjectModification: 2017_07_26-PM-06_45_51

Theory : rationals


Home Index