Nuprl Definition : ss-open-and
A ⋂ B == λz.∃u,v:ss-basic(X). ((A u) ∧ (B v) ∧ (z = ss-basic-and(u;v) ∈ ss-basic(X)))
Definitions occuring in Statement :
ss-basic-and: ss-basic-and(u;v),
ss-basic: ss-basic(X),
exists: ∃x:A. B[x],
and: P ∧ Q,
apply: f a,
lambda: λx.A[x],
equal: s = t ∈ T
Definitions occuring in definition :
lambda: λx.A[x],
exists: ∃x:A. B[x],
and: P ∧ Q,
apply: f a,
equal: s = t ∈ T,
ss-basic: ss-basic(X),
ss-basic-and: ss-basic-and(u;v)
FDL editor aliases :
ss-open-and
Latex:
A \mcap{} B == \mlambda{}z.\mexists{}u,v:ss-basic(X). ((A u) \mwedge{} (B v) \mwedge{} (z = ss-basic-and(u;v)))
Date html generated:
2020_05_20-PM-01_22_33
Last ObjectModification:
2018_07_06-PM-04_49_06
Theory : intuitionistic!topology
Home
Index