Nuprl Lemma : convex-comb_wf1
∀[x,y,r:ℝ]. ∀[s:{s:ℝ| r + s ≠ r0} ]. (convex-comb(x;y;r;s) ∈ ℝ)
Proof
Definitions occuring in Statement :
convex-comb: convex-comb(x;y;r;s),
rneq: x ≠ y,
radd: a + b,
int-to-real: r(n),
real: ℝ,
uall: ∀[x:A]. B[x],
member: t ∈ T,
set: {x:A| B[x]} ,
natural_number: $n
Definitions unfolded in proof :
so_apply: x[s],
so_lambda: λ2x.t[x],
prop: ℙ,
uimplies: b supposing a,
convex-comb: convex-comb(x;y;r;s),
member: t ∈ T,
uall: ∀[x:A]. B[x]
Lemmas referenced :
int-to-real_wf,
rneq_wf,
real_wf,
set_wf,
rmul_wf,
radd_wf,
rdiv_wf
Rules used in proof :
because_Cache,
isect_memberEquality,
natural_numberEquality,
lambdaEquality,
equalitySymmetry,
equalityTransitivity,
axiomEquality,
independent_isectElimination,
hypothesis,
hypothesisEquality,
isectElimination,
sqequalHypSubstitution,
extract_by_obid,
sqequalRule,
rename,
thin,
setElimination,
cut,
introduction,
isect_memberFormation,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution
Latex:
\mforall{}[x,y,r:\mBbbR{}]. \mforall{}[s:\{s:\mBbbR{}| r + s \mneq{} r0\} ]. (convex-comb(x;y;r;s) \mmember{} \mBbbR{})
Date html generated:
2017_10_04-PM-11_10_56
Last ObjectModification:
2017_07_29-PM-08_07_19
Theory : reals_2
Home
Index