Nuprl Definition : ss-open-or
⋃x:T.F[x] == λB.∃x:T. (F[x] B)
Definitions occuring in Statement :
exists: ∃x:A. B[x],
apply: f a,
lambda: λx.A[x]
Definitions occuring in definition :
lambda: λx.A[x],
exists: ∃x:A. B[x],
apply: f a
FDL editor aliases :
ss-open-or
Latex:
\mcup{}x:T.F[x] == \mlambda{}B.\mexists{}x:T. (F[x] B)
Date html generated:
2020_05_20-PM-01_22_40
Last ObjectModification:
2018_07_06-PM-04_59_00
Theory : intuitionistic!topology
Home
Index