Nuprl Definition : ss-homeo
ss-homeo(X;Y) == ∃f:Point(X ⟶ Y). ∃g:Point(Y ⟶ X). ((∀x:Point(X). g(f(x)) ≡ x) ∧ (∀y:Point(Y). f(g(y)) ≡ y))
Definitions occuring in Statement :
ss-ap: f(x),
ss-fun: X ⟶ Y,
ss-eq: x ≡ y,
ss-point: Point(ss),
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
and: P ∧ Q
Definitions occuring in definition :
exists: ∃x:A. B[x],
ss-fun: X ⟶ Y,
and: P ∧ Q,
all: ∀x:A. B[x],
ss-point: Point(ss),
ss-eq: x ≡ y,
ss-ap: f(x)
FDL editor aliases :
ss-homeo
Latex:
ss-homeo(X;Y) ==
\mexists{}f:Point(X {}\mrightarrow{} Y). \mexists{}g:Point(Y {}\mrightarrow{} X). ((\mforall{}x:Point(X). g(f(x)) \mequiv{} x) \mwedge{} (\mforall{}y:Point(Y). f(g(y)) \mequiv{} y))
Date html generated:
2020_05_20-PM-01_19_52
Last ObjectModification:
2018_07_04-PM-00_13_57
Theory : intuitionistic!topology
Home
Index