Nuprl Lemma : real-ss-eq
∀[x,y:ℝ]. uiff(x ≡ y;x = y)
Proof
Definitions occuring in Statement :
real-ss: ℝ,
ss-eq: x ≡ y,
req: x = y,
real: ℝ,
uiff: uiff(P;Q),
uall: ∀[x:A]. B[x]
Definitions unfolded in proof :
false: False,
prop: ℙ,
not: ¬A,
implies: P ⇒ Q,
uimplies: b supposing a,
and: P ∧ Q,
uiff: uiff(P;Q),
uall: ∀[x:A]. B[x],
btrue: tt,
bfalse: ff,
ifthenelse: if b then t else f fi ,
eq_atom: x =a y,
member: t ∈ T,
all: ∀x:A. B[x],
ss-sep: x # y,
mk-ss: Point=P #=Sep cotrans=C,
ss-eq: x ≡ y,
real-ss: ℝ
Lemmas referenced :
real_wf,
req_wf,
req-iff-not-rneq,
istype-void,
rneq_wf,
req_witness,
not-rneq,
rec_select_update_lemma
Rules used in proof :
isectIsTypeImplies,
isect_memberEquality_alt,
independent_pairEquality,
inhabitedIsType,
functionIsTypeImplies,
lambdaEquality_alt,
because_Cache,
voidElimination,
productElimination,
lambdaFormation_alt,
universeIsType,
functionIsType,
independent_functionElimination,
independent_isectElimination,
hypothesisEquality,
isectElimination,
independent_pairFormation,
isect_memberFormation_alt,
hypothesis,
Error :memTop,
thin,
dependent_functionElimination,
sqequalHypSubstitution,
extract_by_obid,
introduction,
cut,
sqequalRule,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution
Latex:
\mforall{}[x,y:\mBbbR{}]. uiff(x \mequiv{} y;x = y)
Date html generated:
2020_05_20-PM-01_19_50
Last ObjectModification:
2019_12_28-AM-10_59_06
Theory : constructive!algebra
Home
Index