Nuprl Lemma : qle-qavg-iff-6

[a,b,c:ℚ].  uiff(qavg(a;b) ≤ qavg(c;a);b ≤ c)


Proof




Definitions occuring in Statement :  qavg: qavg(a;b) qle: r ≤ s rationals: uiff: uiff(P;Q) uall: [x:A]. B[x]
Definitions unfolded in proof :  rev_implies:  Q rev_uimplies: rev_uimplies(P;Q) bnot: ¬bb dset_of_mon: g↓set oset_of_ocmon: g↓oset set_le: b band: p ∧b q set_blt: a <b b set_lt: a <b grp_lt: a < b qless: r < s iff: ⇐⇒ Q squash: T guard: {T} true: True lt_int: i <j qmul: s qadd: s qsub: s qpositive: qpositive(r) bor: p ∨bq q_le: q_le(r;s) qadd_grp: <ℚ+> pi2: snd(t) pi1: fst(t) grp_le: b infix_ap: y grp_leq: a ≤ b qle: r ≤ s prop: false: False assert: b bfalse: ff eq_int: (i =z j) btrue: tt ifthenelse: if then else fi  evalall: evalall(t) callbyvalueall: callbyvalueall qeq: qeq(r;s) not: ¬A subtype_rel: A ⊆B implies:  Q uimplies: supposing a and: P ∧ Q uiff: uiff(P;Q) member: t ∈ T uall: [x:A]. B[x] qavg: qavg(a;b)
Lemmas referenced :  qmul_preserves_qle iff_weakening_equal qmul-qdiv-cancel subtype_rel_self qadd_comm_q equal-wf-T-base not_wf true_wf squash_wf qadd_inv_assoc_q qadd_ac_1_q qadd_preserves_qle uiff_transitivity2 qmul_wf qmul_preserves_qle2 rationals_wf assert-qeq qadd_wf qdiv_wf qle_wf qle_witness
Rules used in proof :  universeEquality instantiate imageMemberEquality imageElimination lambdaEquality_alt minusEquality isectIsTypeImplies isect_memberEquality_alt independent_pairEquality sqequalBase baseClosed inhabitedIsType equalityIstype voidElimination productElimination equalitySymmetry equalityTransitivity lambdaFormation_alt independent_isectElimination because_Cache applyEquality natural_numberEquality universeIsType hypothesis independent_functionElimination hypothesisEquality thin isectElimination sqequalHypSubstitution extract_by_obid independent_pairFormation cut introduction isect_memberFormation_alt computationStep sqequalTransitivity sqequalReflexivity sqequalRule sqequalSubstitution

Latex:
\mforall{}[a,b,c:\mBbbQ{}].    uiff(qavg(a;b)  \mleq{}  qavg(c;a);b  \mleq{}  c)



Date html generated: 2019_10_29-AM-07_45_51
Last ObjectModification: 2019_10_21-PM-08_56_18

Theory : rationals


Home Index