Nuprl Lemma : qavg-eq-iff-5
∀[a,b,c:ℚ]. uiff(qavg(b;a) = qavg(a;c) ∈ ℚ;b = c ∈ ℚ)
Proof
Definitions occuring in Statement :
qavg: qavg(a;b),
rationals: ℚ,
uiff: uiff(P;Q),
uall: ∀[x:A]. B[x],
equal: s = t ∈ T
Definitions unfolded in proof :
qavg: qavg(a;b),
uall: ∀[x:A]. B[x],
member: t ∈ T,
uiff: uiff(P;Q),
and: P ∧ Q,
uimplies: b supposing a,
subtype_rel: A ⊆r B,
not: ¬A,
implies: P ⇒ Q,
qeq: qeq(r;s),
callbyvalueall: callbyvalueall,
evalall: evalall(t),
ifthenelse: if b then t else f fi ,
btrue: tt,
eq_int: (i =z j),
bfalse: ff,
assert: ↑b,
false: False,
squash: ↓T,
prop: ℙ,
true: True,
guard: {T},
iff: P ⇐⇒ Q,
rev_implies: P ⇐ Q
Lemmas referenced :
qdiv_wf,
qadd_wf,
int-subtype-rationals,
assert-qeq,
equal_wf,
squash_wf,
true_wf,
istype-universe,
not_wf,
equal-wf-T-base,
rationals_wf,
qadd_com,
subtype_rel_self,
iff_weakening_equal,
qmul_wf,
qadd_comm_q,
qmul-qdiv-cancel,
qadd_ac_1_q,
qadd_inv_assoc_q
Rules used in proof :
sqequalSubstitution,
sqequalRule,
sqequalReflexivity,
sqequalTransitivity,
computationStep,
isect_memberFormation_alt,
introduction,
cut,
independent_pairFormation,
hypothesis,
equalityIstype,
inhabitedIsType,
hypothesisEquality,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
closedConclusion,
natural_numberEquality,
applyEquality,
independent_isectElimination,
lambdaFormation_alt,
equalityTransitivity,
equalitySymmetry,
productElimination,
voidElimination,
baseClosed,
sqequalBase,
because_Cache,
lambdaEquality_alt,
imageElimination,
universeIsType,
instantiate,
universeEquality,
imageMemberEquality,
independent_functionElimination,
independent_pairEquality,
isect_memberEquality_alt,
axiomEquality,
isectIsTypeImplies,
minusEquality,
applyLambdaEquality
Latex:
\mforall{}[a,b,c:\mBbbQ{}]. uiff(qavg(b;a) = qavg(a;c);b = c)
Date html generated:
2020_05_20-AM-09_16_58
Last ObjectModification:
2020_01_04-PM-10_19_27
Theory : rationals
Home
Index