Nuprl Lemma : homeo-image-homeomorphic
∀[X,Y:Type]. ∀[dX:metric(X)]. ∀[dY:metric(Y)].
∀h:homeomorphic(X;dX;Y;dY). ∀[A:Type]. homeomorphic(A;dX;homeo-image(A;Y;dY;h);dY) supposing metric-subspace(X;dX;A)
Proof
Definitions occuring in Statement :
homeo-image: homeo-image(A;Y;dY;h),
metric-subspace: metric-subspace(X;d;A),
homeomorphic: homeomorphic(X;dX;Y;dY),
metric: metric(X),
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
universe: Type
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
all: ∀x:A. B[x],
uimplies: b supposing a,
metric-subspace: metric-subspace(X;d;A),
and: P ∧ Q,
implies: P ⇒ Q,
prop: ℙ
Latex:
\mforall{}[X,Y:Type]. \mforall{}[dX:metric(X)]. \mforall{}[dY:metric(Y)].
\mforall{}h:homeomorphic(X;dX;Y;dY)
\mforall{}[A:Type]. homeomorphic(A;dX;homeo-image(A;Y;dY;h);dY) supposing metric-subspace(X;dX;A)
Date html generated:
2020_05_20-AM-11_52_11
Last ObjectModification:
2019_11_07-PM-02_45_47
Theory : reals
Home
Index