Nuprl Lemma : homeomorphic_functionality
∀[X,Y,X',Y':Type].
(∀[dX:metric(X)]. ∀[dY:metric(Y)]. homeomorphic(X;dX;Y;dY) ≡ homeomorphic(X';dX;Y';dY)) supposing (X ≡ X' and Y ≡ Y')
Proof
Definitions occuring in Statement :
homeomorphic: homeomorphic(X;dX;Y;dY),
metric: metric(X),
ext-eq: A ≡ B,
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
universe: Type
Definitions unfolded in proof :
ext-eq: A ≡ B,
uall: ∀[x:A]. B[x],
uimplies: b supposing a,
and: P ∧ Q,
member: t ∈ T,
prop: ℙ,
subtype_rel: A ⊆r B,
sq_stable: SqStable(P),
implies: P ⇒ Q,
homeomorphic: homeomorphic(X;dX;Y;dY),
sq_exists: ∃x:A [B[x]],
exists: ∃x:A. B[x],
mfun: FUN(X ⟶ Y),
so_lambda: λ2x.t[x],
so_apply: x[s],
all: ∀x:A. B[x],
is-mfun: f:FUN(X;Y),
cand: A c∧ B,
squash: ↓T,
guard: {T}
Latex:
\mforall{}[X,Y,X',Y':Type].
(\mforall{}[dX:metric(X)]. \mforall{}[dY:metric(Y)].
homeomorphic(X;dX;Y;dY) \mequiv{} homeomorphic(X';dX;Y';dY)) supposing
(X \mequiv{} X' and
Y \mequiv{} Y')
Date html generated:
2020_05_20-AM-11_41_13
Last ObjectModification:
2019_11_11-PM-05_09_11
Theory : reals
Home
Index