Further properties of homeomorphisms #
This file proves further properties of homeomorphisms between topological spaces. Pretty much every topological property is preserved under homeomorphisms.
Homeomorphism given an embedding.
Equations
- Homeomorph.ofIsEmbedding f hf = { toEquiv := Equiv.ofInjective f ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }
Alias of Homeomorph.ofIsEmbedding
.
Homeomorphism given an embedding.
Equations
If h : X → Y
is a homeomorphism, h(s)
is compact iff s
is.
If h : X → Y
is a homeomorphism, h⁻¹(s)
is compact iff s
is.
If h : X → Y
is a homeomorphism, s
is σ-compact iff h(s)
is.
If h : X → Y
is a homeomorphism, h⁻¹(s)
is σ-compact iff s
is.
If the codomain of a homeomorphism is a locally connected space, then the domain is also a locally connected space.
The codomain of a homeomorphism is a locally compact space if and only if the domain is a locally compact space.
A homeomorphism h : X ≃ₜ Y
lifts to a homeomorphism between subtypes corresponding to
predicates p : X → Prop
and q : Y → Prop
so long as p = q ∘ h
.
Equations
- h.subtype h_iff = { toEquiv := h.subtypeEquiv h_iff, continuous_toFun := ⋯, continuous_invFun := ⋯ }
A homeomorphism h : X ≃ₜ Y
lifts to a homeomorphism between sets s : Set X
and t : Set Y
whenever h
maps s
onto t
.
If two sets are equal, then they are homeomorphic.
Equations
- Homeomorph.setCongr h = { toEquiv := Equiv.setCongr h, continuous_toFun := ⋯, continuous_invFun := ⋯ }
The product over S ⊕ T
of a family of topological spaces
is homeomorphic to the product of (the product over S
) and (the product over T
).
This is Equiv.sumPiEquivProdPi
as a Homeomorph
.
Equations
- Homeomorph.sumPiEquivProdPi S T A = { toEquiv := Equiv.sumPiEquivProdPi A, continuous_toFun := ⋯, continuous_invFun := ⋯ }
The product Π t : α, f t
of a family of topological spaces is homeomorphic to the
space f ⬝
when α
only contains ⬝
.
This is Equiv.piUnique
as a Homeomorph
.
Equations
Equiv.piCongrLeft
as a homeomorphism: this is the natural homeomorphism
Π i, Y (e i) ≃ₜ Π j, Y j
obtained from a bijection ι ≃ ι'
.
Equations
- Homeomorph.piCongrLeft e = { toEquiv := Equiv.piCongrLeft Y e, continuous_toFun := ⋯, continuous_invFun := ⋯ }
Equiv.piCongrRight
as a homeomorphism: this is the natural homeomorphism
Π i, Y₁ i ≃ₜ Π j, Y₂ i
obtained from homeomorphisms Y₁ i ≃ₜ Y₂ i
for each i
.
Equations
- Homeomorph.piCongrRight F = { toEquiv := Equiv.piCongrRight fun (i : ι) => (F i).toEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }
Equiv.piCongr
as a homeomorphism: this is the natural homeomorphism
Π i₁, Y₁ i ≃ₜ Π i₂, Y₂ i₂
obtained from a bijection ι₁ ≃ ι₂
and homeomorphisms
Y₁ i₁ ≃ₜ Y₂ (e i₁)
for each i₁ : ι₁
.
Equations
ULift X
is homeomorphic to X
.
Equations
- Homeomorph.ulift = { toEquiv := Equiv.ulift, continuous_toFun := ⋯, continuous_invFun := ⋯ }
The natural homeomorphism (ι ⊕ ι' → X) ≃ₜ (ι → X) × (ι' → X)
.
Equiv.sumArrowEquivProdArrow
as a homeomorphism.
Equations
- Homeomorph.sumArrowHomeomorphProdArrow = { toEquiv := Equiv.sumArrowEquivProdArrow ι ι' X, continuous_toFun := ⋯, continuous_invFun := ⋯ }
The natural homeomorphism between (Fin m → X) × (Fin n → X)
and Fin (m + n) → X
.
Fin.appendEquiv
as a homeomorphism
Equations
- Fin.appendHomeomorph m n = { toEquiv := Fin.appendEquiv m n, continuous_toFun := ⋯, continuous_invFun := ⋯ }
(Σ i, X i) × Y
is homeomorphic to Σ i, (X i × Y)
.
Equations
If ι
has a unique element, then ι → X
is homeomorphic to X
.
Equations
- Homeomorph.funUnique ι X = { toEquiv := Equiv.funUnique ι X, continuous_toFun := ⋯, continuous_invFun := ⋯ }
Homeomorphism between dependent functions Π i : Fin 2, X i
and X 0 × X 1
.
Equations
- Homeomorph.piFinTwo X = { toEquiv := piFinTwoEquiv X, continuous_toFun := ⋯, continuous_invFun := ⋯ }
Homeomorphism between X² = Fin 2 → X
and X × X
.
Equations
- Homeomorph.finTwoArrow = { toEquiv := finTwoArrowEquiv X, continuous_toFun := ⋯, continuous_invFun := ⋯ }
A subset of a topological space is homeomorphic to its image under a homeomorphism.
Set.univ X
is homeomorphic to X
.
Equations
- Homeomorph.Set.univ X = { toEquiv := Equiv.Set.univ X, continuous_toFun := ⋯, continuous_invFun := ⋯ }
s ×ˢ t
is homeomorphic to s × t
.
Equations
- Homeomorph.Set.prod s t = { toEquiv := Equiv.Set.prod s t, continuous_toFun := ⋯, continuous_invFun := ⋯ }
The topological space Π i, Y i
can be split as a product by separating the indices in ι
depending on whether they satisfy a predicate p or not.
Equations
- Homeomorph.piEquivPiSubtypeProd p Y = { toEquiv := Equiv.piEquivPiSubtypeProd p Y, continuous_toFun := ⋯, continuous_invFun := ⋯ }
A product of topological spaces can be split as the binary product of one of the spaces and the product of all the remaining spaces.
Equations
- Homeomorph.piSplitAt i Y = { toEquiv := Equiv.piSplitAt i Y, continuous_toFun := ⋯, continuous_invFun := ⋯ }
A product of copies of a topological space can be split as the binary product of one copy and the product of all the remaining copies.
Equations
- Homeomorph.funSplitAt Y i = Homeomorph.piSplitAt i fun (a : ι) => Y
Continuous equivalences from a compact space to a T2 space are homeomorphisms.
This is not true when T2 is weakened to T1
(see Continuous.homeoOfEquivCompactToT2.t1_counterexample
).
Equations
- hf.homeoOfEquivCompactToT2 = { toEquiv := f, continuous_toFun := hf, continuous_invFun := ⋯ }
Predicate saying that f
is a homeomorphism.
This should be used only when f
is a concrete function whose continuous inverse is not easy to
write down. Otherwise, Homeomorph
should be preferred as it bundles the continuous inverse.
Having both Homeomorph
and IsHomeomorph
is justified by the fact that so many function
properties are unbundled in the topology part of the library, and by the fact that a homeomorphism
is not merely a continuous bijection, that is IsHomeomorph f
is not equivalent to
Continuous f ∧ Bijective f
but to Continuous f ∧ Bijective f ∧ IsOpenMap f
.
- continuous : Continuous f
- isOpenMap : IsOpenMap f
- bijective : Function.Bijective f
Bundled homeomorphism constructed from a map that is a homeomorphism.
Equations
- IsHomeomorph.homeomorph f hf = { toEquiv := Equiv.ofBijective f ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }
Alias of IsHomeomorph.isInducing
.
Alias of IsHomeomorph.isEmbedding
.
Alias of IsHomeomorph.isQuotientMap
.
Alias of IsHomeomorph.isClosedEmbedding
.
Alias of IsHomeomorph.isOpenEmbedding
.
A map is a homeomorphism iff it is the map underlying a bundled homeomorphism h : X ≃ₜ Y
.
A map is a homeomorphism iff it is continuous and has a continuous inverse.
A map is a homeomorphism iff it is a surjective embedding.
Alias of isHomeomorph_iff_isEmbedding_surjective
.
A map is a homeomorphism iff it is a surjective embedding.
A map is a homeomorphism iff it is continuous, closed and bijective.
A map from a compact space to a T2 space is a homeomorphism iff it is continuous and bijective.