Nuprl Lemma : convex-comb_functionality
∀[x1,y1,r1,x2,y2,r2:ℝ]. ∀[s1:{s:ℝ| r1 + s ≠ r0} ]. ∀[s2:{s:ℝ| r2 + s ≠ r0} ].
(convex-comb(x1;y1;r1;s1) = convex-comb(x2;y2;r2;s2)) supposing ((s1 = s2) and (r1 = r2) and (y1 = y2) and (x1 = x2))
Proof
Definitions occuring in Statement :
convex-comb: convex-comb(x;y;r;s),
rneq: x ≠ y,
req: x = y,
radd: a + b,
int-to-real: r(n),
real: ℝ,
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
set: {x:A| B[x]} ,
natural_number: $n
Definitions unfolded in proof :
so_apply: x[s],
so_lambda: λ2x.t[x],
prop: ℙ,
squash: ↓T,
implies: P ⇒ Q,
sq_stable: SqStable(P),
all: ∀x:A. B[x],
convex-comb: convex-comb(x;y;r;s),
uimplies: b supposing a,
member: t ∈ T,
uall: ∀[x:A]. B[x]
Lemmas referenced :
real_wf,
set_wf,
req_wf,
rneq_wf,
convex-comb_wf1,
req_witness,
rmul_functionality,
radd_functionality,
sq_stable__req,
int-to-real_wf,
sq_stable_rneq,
rmul_wf,
radd_wf,
rdiv_functionality
Rules used in proof :
lambdaEquality,
equalitySymmetry,
equalityTransitivity,
isect_memberEquality,
dependent_set_memberEquality,
imageElimination,
baseClosed,
imageMemberEquality,
sqequalRule,
independent_functionElimination,
natural_numberEquality,
dependent_functionElimination,
independent_isectElimination,
because_Cache,
rename,
setElimination,
hypothesis,
hypothesisEquality,
thin,
isectElimination,
sqequalHypSubstitution,
extract_by_obid,
cut,
introduction,
isect_memberFormation,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution
Latex:
\mforall{}[x1,y1,r1,x2,y2,r2:\mBbbR{}]. \mforall{}[s1:\{s:\mBbbR{}| r1 + s \mneq{} r0\} ]. \mforall{}[s2:\{s:\mBbbR{}| r2 + s \mneq{} r0\} ].
(convex-comb(x1;y1;r1;s1) = convex-comb(x2;y2;r2;s2)) supposing
((s1 = s2) and
(r1 = r2) and
(y1 = y2) and
(x1 = x2))
Date html generated:
2017_10_04-PM-11_12_01
Last ObjectModification:
2017_07_30-AM-11_24_16
Theory : reals_2
Home
Index