Nuprl Lemma : ss-basic-and_wf
∀[X:SeparationSpace]. ∀[u,v:ss-basic(X)]. (ss-basic-and(u;v) ∈ ss-basic(X))
Proof
Definitions occuring in Statement :
ss-basic-and: ss-basic-and(u;v),
ss-basic: ss-basic(X),
separation-space: SeparationSpace,
uall: ∀[x:A]. B[x],
member: t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
ss-basic-and: ss-basic-and(u;v),
ss-basic: ss-basic(X),
subtype_rel: A ⊆r B
Lemmas referenced :
append_wf,
ss-point_wf,
ss-fun_wf,
real-ss_wf,
real_wf,
subtype_rel_self,
ss-basic_wf,
separation-space_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation_alt,
introduction,
cut,
sqequalRule,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
productEquality,
hypothesisEquality,
hypothesis,
applyEquality,
because_Cache,
axiomEquality,
equalityTransitivity,
equalitySymmetry,
inhabitedIsType,
isect_memberEquality_alt,
isectIsTypeImplies,
universeIsType
Latex:
\mforall{}[X:SeparationSpace]. \mforall{}[u,v:ss-basic(X)]. (ss-basic-and(u;v) \mmember{} ss-basic(X))
Date html generated:
2020_05_20-PM-01_22_17
Last ObjectModification:
2020_02_08-AM-11_38_57
Theory : intuitionistic!topology
Home
Index