Nuprl Lemma : ss-mem-basic_wf
∀[X:SeparationSpace]. ∀[B:ss-basic(X)]. ∀[x:Point(X)]. (x ∈ B ∈ ℙ)
Proof
Definitions occuring in Statement :
ss-mem-basic: x ∈ B,
ss-basic: ss-basic(X),
ss-point: Point(ss),
separation-space: SeparationSpace,
uall: ∀[x:A]. B[x],
prop: ℙ,
member: t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
ss-mem-basic: x ∈ B,
ss-basic: ss-basic(X),
so_lambda: λ2x.t[x],
subtype_rel: A ⊆r B,
ss-point: Point(ss),
record-select: r.x,
real-ss: ℝ,
mk-ss: Point=P #=Sep cotrans=C,
record-update: r[x := v],
ifthenelse: if b then t else f fi ,
eq_atom: x =a y,
bfalse: ff,
btrue: tt,
real: ℝ,
prop: ℙ,
so_apply: x[s]
Lemmas referenced :
l_all_wf2,
ss-point_wf,
ss-fun_wf,
real-ss_wf,
real_wf,
rless_wf,
ss-ap_wf,
subtype_rel_self,
l_member_wf,
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,
lambdaEquality_alt,
spreadEquality,
setElimination,
rename,
applyEquality,
setIsType,
productIsType,
universeIsType,
axiomEquality,
equalityTransitivity,
equalitySymmetry,
isect_memberEquality_alt,
isectIsTypeImplies,
inhabitedIsType
Latex:
\mforall{}[X:SeparationSpace]. \mforall{}[B:ss-basic(X)]. \mforall{}[x:Point(X)]. (x \mmember{} B \mmember{} \mBbbP{})
Date html generated:
2020_05_20-PM-01_21_51
Last ObjectModification:
2020_02_08-AM-11_39_00
Theory : intuitionistic!topology
Home
Index