Nuprl Lemma : homeomorphic_inversion
∀[X,Y:Type]. ∀[dX:metric(X)]. ∀[dY:metric(Y)]. (homeomorphic(X;dX;Y;dY) ⇒ homeomorphic(Y;dY;X;dX))
Proof
Definitions occuring in Statement :
homeomorphic: homeomorphic(X;dX;Y;dY),
metric: metric(X),
uall: ∀[x:A]. B[x],
implies: P ⇒ Q,
universe: Type
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
implies: P ⇒ Q,
member: t ∈ T,
prop: ℙ
Latex:
\mforall{}[X,Y:Type]. \mforall{}[dX:metric(X)]. \mforall{}[dY:metric(Y)]. (homeomorphic(X;dX;Y;dY) {}\mRightarrow{} homeomorphic(Y;dY;X;dX))
Date html generated:
2020_05_20-AM-11_42_10
Last ObjectModification:
2019_11_12-AM-09_55_21
Theory : reals
Home
Index