Nuprl Definition : ss-whole
ss-whole(X) == λB.(B = ss-basic-whole() ∈ ss-basic(X))
Definitions occuring in Statement :
ss-basic-whole: ss-basic-whole(),
ss-basic: ss-basic(X),
lambda: λx.A[x],
equal: s = t ∈ T
Definitions occuring in definition :
lambda: λx.A[x],
equal: s = t ∈ T,
ss-basic: ss-basic(X),
ss-basic-whole: ss-basic-whole()
FDL editor aliases :
ss-whole
Latex:
ss-whole(X) == \mlambda{}B.(B = ss-basic-whole())
Date html generated:
2020_05_20-PM-01_22_26
Last ObjectModification:
2018_07_06-PM-02_22_48
Theory : intuitionistic!topology
Home
Index