Nuprl Lemma : qavg-eq-iff-3

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


Proof




Definitions occuring in Statement :  qavg: qavg(a;b) rationals: uiff: uiff(P;Q) uall: [x:A]. B[x] equal: t ∈ T
Definitions unfolded in proof :  rev_implies:  Q rev_uimplies: rev_uimplies(P;Q) qadd: s iff: ⇐⇒ Q guard: {T} prop: squash: T true: True 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) implies:  Q not: ¬A subtype_rel: A ⊆B 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_ident qmul-preserves-eq qmul_one_qrng q_distrib qadd_inv_assoc_q qadd_ac_1_q iff_weakening_equal qmul-qdiv-cancel subtype_rel_self qadd_comm_q equal-wf-T-base not_wf istype-universe true_wf squash_wf equal_wf int-subtype-rationals qmul_wf rationals_wf assert-qeq qadd_wf qdiv_wf
Rules used in proof :  independent_functionElimination imageMemberEquality universeEquality instantiate imageElimination lambdaEquality_alt minusEquality applyLambdaEquality universeIsType isectIsTypeImplies axiomEquality isect_memberEquality_alt independent_pairEquality sqequalBase baseClosed voidElimination productElimination equalitySymmetry equalityTransitivity lambdaFormation_alt independent_isectElimination because_Cache applyEquality natural_numberEquality thin isectElimination sqequalHypSubstitution extract_by_obid hypothesisEquality inhabitedIsType equalityIstype hypothesis independent_pairFormation cut introduction isect_memberFormation_alt computationStep sqequalTransitivity sqequalReflexivity sqequalRule sqequalSubstitution

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



Date html generated: 2019_10_29-AM-07_44_42
Last ObjectModification: 2019_10_21-PM-08_26_25

Theory : rationals


Home Index