Nuprl Definition : ss-mem-open
x ∈ O == ∃B:ss-basic(X). ((O B) ∧ x ∈ B)
Definitions occuring in Statement :
ss-mem-basic: x ∈ B,
ss-basic: ss-basic(X),
exists: ∃x:A. B[x],
and: P ∧ Q,
apply: f a
Definitions occuring in definition :
exists: ∃x:A. B[x],
ss-basic: ss-basic(X),
and: P ∧ Q,
apply: f a,
ss-mem-basic: x ∈ B
FDL editor aliases :
ss-mem-open
Latex:
x \mmember{} O == \mexists{}B:ss-basic(X). ((O B) \mwedge{} x \mmember{} B)
Date html generated:
2020_05_20-PM-01_22_00
Last ObjectModification:
2018_07_06-PM-01_53_13
Theory : intuitionistic!topology
Home
Index