Nuprl Definition : homeomorphic

homeomorphic(X;dX;Y;dY) ==  ∃f:FUN(X ⟶ Y). (∃g:FUN(Y ⟶ X) [((∀x:X. g (f x) ≡ x) ∧ (∀y:Y. f (g y) ≡ y))])


Definitions occuring in Statement :  mfun: FUN(X ⟶ Y),  meq: x ≡ y,  all: ∀x:A. B[x],  sq_exists: ∃x:A [B[x]],  exists: ∃x:A. B[x],  and: P ∧ Q,  apply: f a
FDL editor aliases :  homeomorphic
Latex:
homeomorphic(X;dX;Y;dY)  ==
    \mexists{}f:FUN(X  {}\mrightarrow{}  Y).  (\mexists{}g:FUN(Y  {}\mrightarrow{}  X)  [((\mforall{}x:X.  g  (f  x)  \mequiv{}  x)  \mwedge{}  (\mforall{}y:Y.  f  (g  y)  \mequiv{}  y))])


Date html generated: 2020_05_20-AM-11_40_52
Last ObjectModification: 2019_11_07-PM-01_38_55

Theory : reals


Home Index