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))])
∧ (∃B:ℕ+ [(∀x1,x2:X. (mdist(dY;f x1;f x2) ≤ (r(B) * mdist(dX;x1;x2))))]))
Definitions occuring in Statement :
mfun: FUN(X ⟶ Y),
mdist: mdist(d;x;y),
meq: x ≡ y,
rleq: x ≤ y,
rmul: a * b,
int-to-real: r(n),
nat_plus: ℕ+,
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))])
\mwedge{} (\mexists{}B:\mBbbN{}\msupplus{} [(\mforall{}x1,x2:X. (mdist(dY;f x1;f x2) \mleq{} (r(B) * mdist(dX;x1;x2))))]))
Date html generated:
2020_05_20-AM-11_42_29
Last ObjectModification:
2019_11_25-PM-02_21_10
Theory : reals
Home
Index