Nuprl Lemma : real-ss_wf
ℝ ∈ SeparationSpace
Proof
Definitions occuring in Statement :
real-ss: ℝ,
separation-space: SeparationSpace,
member: t ∈ T
Definitions unfolded in proof :
real-ss: ℝ,
member: t ∈ T,
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
not: ¬A,
implies: P ⇒ Q,
false: False,
prop: ℙ,
subtype_rel: A ⊆r B,
rneq: x ≠ y,
or: P ∨ Q,
so_lambda: λ2x.t[x],
so_apply: x[s]
Lemmas referenced :
mk-ss_wf,
real_wf,
rneq_wf,
rneq_irrefl,
istype-void,
rneq-cotrans,
subtype_rel_self,
all_wf,
or_wf
Rules used in proof :
sqequalSubstitution,
sqequalRule,
sqequalReflexivity,
sqequalTransitivity,
computationStep,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesis,
dependent_set_memberEquality_alt,
lambdaEquality_alt,
hypothesisEquality,
inhabitedIsType,
universeIsType,
lambdaFormation_alt,
independent_functionElimination,
voidElimination,
functionIsType,
applyEquality,
because_Cache,
instantiate,
functionEquality
Latex:
\mBbbR{} \mmember{} SeparationSpace
Date html generated:
2019_10_31-AM-07_27_15
Last ObjectModification:
2019_09_19-PM-04_13_25
Theory : constructive!algebra
Home
Index