Nuprl Lemma : sq_stable__rv-between
∀n:ℕ. ∀a,b,c:ℝ^n. SqStable(a-b-c)
Proof
Definitions occuring in Statement :
rv-between: a-b-c,
real-vec: ℝ^n,
nat: ℕ,
sq_stable: SqStable(P),
all: ∀x:A. B[x]
Definitions unfolded in proof :
false: False,
not: ¬A,
so_apply: x[s],
so_lambda: λ2x.t[x],
rv-T: rv-T(n;a;b;c),
rev_implies: P ⇐ Q,
and: P ∧ Q,
iff: P ⇐⇒ Q,
squash: ↓T,
uall: ∀[x:A]. B[x],
prop: ℙ,
member: t ∈ T,
implies: P ⇒ Q,
sq_stable: SqStable(P),
all: ∀x:A. B[x]
Lemmas referenced :
stable_real-vec-be,
sq_stable__from_stable,
sq_stable__all,
not_wf,
real-vec-be_wf,
sq_stable__real-vec-sep,
sq_stable__and,
rv-T_wf,
real-vec-sep_wf,
rv-between-iff,
nat_wf,
real-vec_wf,
rv-between_wf,
squash_wf
Rules used in proof :
voidElimination,
lambdaEquality,
functionEquality,
because_Cache,
isect_memberEquality,
productEquality,
promote_hyp,
levelHypothesis,
baseClosed,
imageMemberEquality,
sqequalRule,
independent_functionElimination,
productElimination,
dependent_functionElimination,
imageElimination,
addLevel,
hypothesis,
hypothesisEquality,
thin,
isectElimination,
sqequalHypSubstitution,
extract_by_obid,
introduction,
cut,
lambdaFormation,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution
Latex:
\mforall{}n:\mBbbN{}. \mforall{}a,b,c:\mBbbR{}\^{}n. SqStable(a-b-c)
Date html generated:
2018_05_22-PM-02_28_59
Last ObjectModification:
2018_05_21-AM-00_48_03
Theory : reals
Home
Index