Homeomorphisms #
This file defines homeomorphisms between two topological spaces. They are bijections with both
directions continuous. We denote homeomorphisms with the notation ≃ₜ
.
Main definitions #
Homeomorph X Y
: The type of homeomorphisms fromX
toY
. This type can be denoted using the following notation:X ≃ₜ Y
.
Main results #
- Pretty much every topological property is preserved under homeomorphisms.
Homeomorph.homeomorphOfContinuousOpen
: A continuous bijection that is an open map is a homeomorphism.
Homeomorphism between X
and Y
, also called topological isomorphism
- toFun : X → Y
- invFun : Y → X
- left_inv : Function.LeftInverse self.invFun self.toFun
- right_inv : Function.RightInverse self.invFun self.toFun
- continuous_toFun : Continuous self.toFun
The forward map of a homeomorphism is a continuous function.
- continuous_invFun : Continuous self.invFun
The inverse map of a homeomorphism is a continuous function.
Instances For
The forward map of a homeomorphism is a continuous function.
The inverse map of a homeomorphism is a continuous function.
Homeomorphism between X
and Y
, also called topological isomorphism
Equations
- «term_≃ₜ_» = Lean.ParserDescr.trailingNode `term_≃ₜ_ 25 25 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≃ₜ ") (Lean.ParserDescr.cat `term 26))
Instances For
Equations
- Homeomorph.instCoeFunForall = { coe := DFunLike.coe }
The unique homeomorphism between two empty types.
Equations
- Homeomorph.empty = { toEquiv := Equiv.equivOfIsEmpty X Y, continuous_toFun := ⋯, continuous_invFun := ⋯ }
Instances For
Inverse of a homeomorphism.
Equations
- h.symm = { toEquiv := h.symm, continuous_toFun := ⋯, continuous_invFun := ⋯ }
Instances For
See Note [custom simps projection]
Equations
- Homeomorph.Simps.symm_apply h = ⇑h.symm
Instances For
Identity map as a homeomorphism.
Equations
- Homeomorph.refl X = { toEquiv := Equiv.refl X, continuous_toFun := ⋯, continuous_invFun := ⋯ }
Instances For
Composition of two homeomorphisms.
Equations
- h₁.trans h₂ = { toEquiv := h₁.trans h₂.toEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }
Instances For
Change the homeomorphism f
to make the inverse function definitionally equal to g
.
Equations
- f.changeInv g hg = { toFun := ⇑f, invFun := g, left_inv := ⋯, right_inv := ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }
Instances For
Homeomorphism given an embedding.
Equations
- Homeomorph.ofEmbedding f hf = { toEquiv := Equiv.ofInjective f ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }
Instances For
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.
Alias of Homeomorph.isDenseEmbedding
.
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.
If a bijective map e : X ≃ Y
is continuous and open, then it is a homeomorphism.
Equations
- Homeomorph.homeomorphOfContinuousOpen e h₁ h₂ = { toEquiv := e, continuous_toFun := h₁, continuous_invFun := ⋯ }
Instances For
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 := ⋯ }
Instances For
A homeomorphism h : X ≃ₜ Y
lifts to a homeomorphism between sets s : Set X
and t : Set Y
whenever h
maps s
onto t
.
Equations
- h.sets h_eq = h.subtype ⋯
Instances For
If two sets are equal, then they are homeomorphic.
Equations
- Homeomorph.setCongr h = { toEquiv := Equiv.setCongr h, continuous_toFun := ⋯, continuous_invFun := ⋯ }
Instances For
Sum of two homeomorphisms.
Equations
- h₁.sumCongr h₂ = { toEquiv := h₁.sumCongr h₂.toEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }
Instances For
Product of two homeomorphisms.
Equations
- h₁.prodCongr h₂ = { toEquiv := h₁.prodCongr h₂.toEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }
Instances For
X ⊕ Y
is homeomorphic to Y ⊕ X
.
Equations
- Homeomorph.sumComm X Y = { toEquiv := Equiv.sumComm X Y, continuous_toFun := ⋯, continuous_invFun := ⋯ }
Instances For
(X ⊕ Y) ⊕ Z
is homeomorphic to X ⊕ (Y ⊕ Z)
.
Equations
- Homeomorph.sumAssoc X Y Z = { toEquiv := Equiv.sumAssoc X Y Z, continuous_toFun := ⋯, continuous_invFun := ⋯ }
Instances For
Four-way commutativity of the disjoint union. The name matches add_add_add_comm
.
Equations
- Homeomorph.sumSumSumComm X Y W Z = { toEquiv := Equiv.sumSumSumComm X Y W Z, continuous_toFun := ⋯, continuous_invFun := ⋯ }
Instances For
The sum of X
with any empty topological space is homeomorphic to X
.
Equations
- Homeomorph.sumEmpty X Y = { toEquiv := Equiv.sumEmpty X Y, continuous_toFun := ⋯, continuous_invFun := ⋯ }
Instances For
The sum of X
with any empty topological space is homeomorphic to X
.
Equations
- Homeomorph.emptySum X Y = (Homeomorph.sumComm Y X).trans (Homeomorph.sumEmpty X Y)
Instances For
X × Y
is homeomorphic to Y × X
.
Equations
- Homeomorph.prodComm X Y = { toEquiv := Equiv.prodComm X Y, continuous_toFun := ⋯, continuous_invFun := ⋯ }
Instances For
(X × Y) × Z
is homeomorphic to X × (Y × Z)
.
Equations
- Homeomorph.prodAssoc X Y Z = { toEquiv := Equiv.prodAssoc X Y Z, continuous_toFun := ⋯, continuous_invFun := ⋯ }
Instances For
Four-way commutativity of prod
. The name matches mul_mul_mul_comm
.
Equations
- Homeomorph.prodProdProdComm X Y W Z = { toEquiv := Equiv.prodProdProdComm X Y W Z, continuous_toFun := ⋯, continuous_invFun := ⋯ }
Instances For
X × {*}
is homeomorphic to X
.
Equations
- Homeomorph.prodPUnit X = { toEquiv := Equiv.prodPUnit X, continuous_toFun := ⋯, continuous_invFun := ⋯ }
Instances For
{*} × X
is homeomorphic to X
.
Equations
- Homeomorph.punitProd X = (Homeomorph.prodComm PUnit.{?u.15 + 1} X).trans (Homeomorph.prodPUnit X)
Instances For
If both X
and Y
have a unique element, then X ≃ₜ Y
.
Equations
- Homeomorph.homeomorphOfUnique X Y = { toEquiv := Equiv.equivOfUnique X Y, continuous_toFun := ⋯, continuous_invFun := ⋯ }
Instances For
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 := ⋯ }
Instances For
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 := ⋯ }
Instances For
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
- Homeomorph.piCongr e F = (Homeomorph.piCongrRight F).trans (Homeomorph.piCongrLeft e)
Instances For
(X ⊕ Y) × Z
is homeomorphic to X × Z ⊕ Y × Z
.
Equations
- Homeomorph.sumProdDistrib = (Homeomorph.homeomorphOfContinuousOpen (Equiv.sumProdDistrib X Y Z).symm ⋯ ⋯).symm
Instances For
X × (Y ⊕ Z)
is homeomorphic to X × Y ⊕ X × Z
.
Equations
- Homeomorph.prodSumDistrib = (Homeomorph.prodComm X (Y ⊕ Z)).trans (Homeomorph.sumProdDistrib.trans ((Homeomorph.prodComm Y X).sumCongr (Homeomorph.prodComm Z X)))
Instances For
(Σ i, X i) × Y
is homeomorphic to Σ i, (X i × Y)
.
Equations
- Homeomorph.sigmaProdDistrib = (Homeomorph.homeomorphOfContinuousOpen (Equiv.sigmaProdDistrib X Y).symm ⋯ ⋯).symm
Instances For
If ι
has a unique element, then ι → X
is homeomorphic to X
.
Equations
- Homeomorph.funUnique ι X = { toEquiv := Equiv.funUnique ι X, continuous_toFun := ⋯, continuous_invFun := ⋯ }
Instances For
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 := ⋯ }
Instances For
Homeomorphism between X² = Fin 2 → X
and X × X
.
Equations
- Homeomorph.finTwoArrow = { toEquiv := finTwoArrowEquiv X, continuous_toFun := ⋯, continuous_invFun := ⋯ }
Instances For
A subset of a topological space is homeomorphic to its image under a homeomorphism.
Equations
- e.image s = { toEquiv := e.image s, continuous_toFun := ⋯, continuous_invFun := ⋯ }
Instances For
Set.univ X
is homeomorphic to X
.
Equations
- Homeomorph.Set.univ X = { toEquiv := Equiv.Set.univ X, continuous_toFun := ⋯, continuous_invFun := ⋯ }
Instances For
s ×ˢ t
is homeomorphic to s × t
.
Equations
- Homeomorph.Set.prod s t = { toEquiv := Equiv.Set.prod s t, continuous_toFun := ⋯, continuous_invFun := ⋯ }
Instances For
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 := ⋯ }
Instances For
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 := ⋯ }
Instances For
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
Instances For
An equiv between topological spaces respecting openness is a homeomorphism.
Equations
- e.toHomeomorph he = { toEquiv := e, continuous_toFun := ⋯, continuous_invFun := ⋯ }
Instances For
An inducing equiv between topological spaces is a homeomorphism.
Equations
- f.toHomeomorphOfInducing hf = { toEquiv := f, continuous_toFun := ⋯, continuous_invFun := ⋯ }
Instances For
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 := ⋯ }
Instances For
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
Instances For
Bundled homeomorphism constructed from a map that is a homeomorphism.
Equations
- IsHomeomorph.homeomorph f hf = { toEquiv := Equiv.ofBijective f ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }
Instances For
Alias of IsHomeomorph.isDenseEmbedding
.
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.
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.