Nuprl Lemma : rn-ss_wf
∀[n:ℕ]. (sepℝ^n ∈ SeparationSpace)
Proof
Definitions occuring in Statement :
rn-ss: sepℝ^n,
nat: ℕ,
uall: ∀[x:A]. B[x],
member: t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
rn-ss: sepℝ^n,
subtype_rel: A ⊆r B,
all: ∀x:A. B[x],
implies: P ⇒ Q,
prop: ℙ,
or: P ∨ Q,
real-vec-sep: a ≠ b,
rless: x < y,
sq_exists: ∃x:A [B[x]],
not: ¬A,
false: False
Lemmas referenced :
Error :mk-ss_wf,
real-vec_wf,
real-vec-sep-cases-alt,
subtype_rel_self,
nat_wf,
real-vec-sep_wf,
istype-nat,
not-real-vec-sep-refl,
istype-void
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation_alt,
introduction,
cut,
sqequalRule,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
hypothesis,
applyEquality,
instantiate,
functionEquality,
unionEquality,
because_Cache,
lambdaEquality_alt,
inhabitedIsType,
universeEquality,
axiomEquality,
equalityTransitivity,
equalitySymmetry,
dependent_set_memberEquality_alt,
universeIsType,
lambdaFormation_alt,
independent_functionElimination,
voidElimination,
functionIsType
Latex:
\mforall{}[n:\mBbbN{}]. (sep\mBbbR{}\^{}n \mmember{} SeparationSpace)
Date html generated:
2020_05_20-PM-01_10_49
Last ObjectModification:
2019_12_10-AM-00_34_41
Theory : inner!product!spaces
Home
Index