Nuprl Lemma : sq_stable__rneq
∀x,y:ℝ. SqStable(x ≠ y)
Proof
Definitions occuring in Statement :
rneq: x ≠ y,
real: ℝ,
sq_stable: SqStable(P),
all: ∀x:A. B[x]
Definitions unfolded in proof :
rev_implies: P ⇐ Q,
and: P ∧ Q,
iff: P ⇐⇒ Q,
implies: P ⇒ Q,
so_apply: x[s],
nat: ℕ,
subtype_rel: A ⊆r B,
real: ℝ,
so_lambda: λ2x.t[x],
member: t ∈ T,
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x]
Lemmas referenced :
real_wf,
decidable__lt,
sq_stable__ex_nat_plus,
rneq-iff,
nat_wf,
subtract_wf,
absval_wf,
less_than_wf,
nat_plus_wf,
exists_wf,
rneq_wf,
sq_stable_functionality
Rules used in proof :
because_Cache,
productElimination,
dependent_functionElimination,
independent_functionElimination,
rename,
setElimination,
applyEquality,
natural_numberEquality,
lambdaEquality,
sqequalRule,
hypothesis,
hypothesisEquality,
thin,
isectElimination,
sqequalHypSubstitution,
extract_by_obid,
introduction,
cut,
lambdaFormation,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution
Latex:
\mforall{}x,y:\mBbbR{}. SqStable(x \mneq{} y)
Date html generated:
2018_05_22-PM-01_21_18
Last ObjectModification:
2018_05_21-AM-00_06_44
Theory : reals
Home
Index