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 from X to Y. 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.

structure Homeomorph (X : Type u_5) (Y : Type u_6) [TopologicalSpace X] [TopologicalSpace Y] extends Equiv : Type (max u_5 u_6)

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.

theorem Homeomorph.continuous_toFun {X : Type u_5} {Y : Type u_6} [TopologicalSpace X] [TopologicalSpace Y] (self : X ≃ₜ Y) : Continuous self.toFun

The forward map of a homeomorphism is a continuous function.

theorem Homeomorph.continuous_invFun {X : Type u_5} {Y : Type u_6} [TopologicalSpace X] [TopologicalSpace Y] (self : X ≃ₜ Y) : Continuous self.invFun

The inverse map of a homeomorphism is a continuous function.

def «term_≃ₜ_» : Lean.TrailingParserDescr

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))

theorem Homeomorph.toEquiv_injective {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] : Function.Injective Homeomorph.toEquiv

instance Homeomorph.instEquivLike {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] : EquivLike (X ≃ₜ Y) X Y

Equations

• Homeomorph.instEquivLike = { coe := fun (h : X ≃ₜ Y) => ⇑h.toEquiv, inv := fun (h : X ≃ₜ Y) => ⇑h.symm, left_inv := ⋯, right_inv := ⋯, coe_injective' := ⋯ }

@[simp]

theorem Homeomorph.homeomorph_mk_coe {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (a : X ≃ Y) (b : Continuous a.toFun) (c : Continuous a.invFun) : ⇑{ toEquiv := a, continuous_toFun := b, continuous_invFun := c } = ⇑a

def Homeomorph.empty {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [IsEmpty X] [IsEmpty Y] : X ≃ₜ Y

The unique homeomorphism between two empty types.

Equations

• Homeomorph.empty = { toEquiv := Equiv.equivOfIsEmpty X Y, continuous_toFun := ⋯, continuous_invFun := ⋯ }

def Homeomorph.symm {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) : Y ≃ₜ X

Inverse of a homeomorphism.

Equations

• h.symm = { toEquiv := h.symm, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem Homeomorph.symm_symm {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) : h.symm.symm = h

theorem Homeomorph.symm_bijective {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] : Function.Bijective Homeomorph.symm

def Homeomorph.Simps.symm_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) : Y → X

See Note [custom simps projection]

Equations

• Homeomorph.Simps.symm_apply h = ⇑h.symm

@[simp]

theorem Homeomorph.coe_toEquiv {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) : ⇑h.toEquiv = ⇑h

@[simp]

theorem Homeomorph.coe_symm_toEquiv {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) : ⇑h.symm = ⇑h.symm

theorem Homeomorph.ext {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {h : X ≃ₜ Y} {h' : X ≃ₜ Y} (H : ∀ (x : X), h x = h' x) : h = h'

def Homeomorph.refl (X : Type u_7) [TopologicalSpace X] : X ≃ₜ X

Identity map as a homeomorphism.

Equations

• Homeomorph.refl X = { toEquiv := Equiv.refl X, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem Homeomorph.refl_apply (X : Type u_7) [TopologicalSpace X] : ⇑(Homeomorph.refl X) = id

def Homeomorph.trans {X : Type u_1} {Y : Type u_2} {Z : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (h₁ : X ≃ₜ Y) (h₂ : Y ≃ₜ Z) : X ≃ₜ Z

Composition of two homeomorphisms.

Equations

• h₁.trans h₂ = { toEquiv := h₁.trans h₂.toEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem Homeomorph.trans_apply {X : Type u_1} {Y : Type u_2} {Z : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (h₁ : X ≃ₜ Y) (h₂ : Y ≃ₜ Z) (x : X) : (h₁.trans h₂) x = h₂ (h₁ x)

@[simp]

theorem Homeomorph.symm_trans_apply {X : Type u_1} {Y : Type u_2} {Z : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (f : X ≃ₜ Y) (g : Y ≃ₜ Z) (z : Z) : (f.trans g).symm z = f.symm (g.symm z)

@[simp]

theorem Homeomorph.homeomorph_mk_coe_symm {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (a : X ≃ Y) (b : Continuous a.toFun) (c : Continuous a.invFun) : ⇑{ toEquiv := a, continuous_toFun := b, continuous_invFun := c }.symm = ⇑a.symm

@[simp]

theorem Homeomorph.refl_symm {X : Type u_1} [TopologicalSpace X] : (Homeomorph.refl X).symm = Homeomorph.refl X

theorem Homeomorph.continuous {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) : Continuous ⇑h

theorem Homeomorph.continuous_symm {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) : Continuous ⇑h.symm

@[simp]

theorem Homeomorph.apply_symm_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) (y : Y) : h (h.symm y) = y

@[simp]

theorem Homeomorph.symm_apply_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) (x : X) : h.symm (h x) = x

@[simp]

theorem Homeomorph.self_trans_symm {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) : h.trans h.symm = Homeomorph.refl X

@[simp]

theorem Homeomorph.symm_trans_self {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) : h.symm.trans h = Homeomorph.refl Y

theorem Homeomorph.bijective {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) : Function.Bijective ⇑h

theorem Homeomorph.injective {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) : Function.Injective ⇑h

theorem Homeomorph.surjective {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) : Function.Surjective ⇑h

def Homeomorph.changeInv {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X ≃ₜ Y) (g : Y → X) (hg : Function.RightInverse g ⇑f) : X ≃ₜ Y

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 := ⋯ }

@[simp]

theorem Homeomorph.symm_comp_self {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) : ⇑h.symm ∘ ⇑h = id

@[simp]

theorem Homeomorph.self_comp_symm {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) : ⇑h ∘ ⇑h.symm = id

@[simp]

theorem Homeomorph.range_coe {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) : Set.range ⇑h = Set.univ

theorem Homeomorph.image_symm {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) : Set.image ⇑h.symm = Set.preimage ⇑h

theorem Homeomorph.preimage_symm {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) : Set.preimage ⇑h.symm = Set.image ⇑h

@[simp]

theorem Homeomorph.image_preimage {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) (s : Set Y) : ⇑h '' (⇑h ⁻¹' s) = s

@[simp]

theorem Homeomorph.preimage_image {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) (s : Set X) : ⇑h ⁻¹' (⇑h '' s) = s

theorem Homeomorph.image_compl {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) (s : Set X) : ⇑h '' sᶜ = (⇑h '' s)ᶜ

theorem Homeomorph.isInducing {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) : IsInducing ⇑h

@[deprecated Homeomorph.isInducing]

theorem Homeomorph.inducing {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) : IsInducing ⇑h

Alias of Homeomorph.isInducing.

theorem Homeomorph.induced_eq {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) : TopologicalSpace.induced (⇑h) inst✝ = inst✝¹

theorem Homeomorph.isQuotientMap {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) : IsQuotientMap ⇑h

@[deprecated Homeomorph.isQuotientMap]

theorem Homeomorph.quotientMap {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) : IsQuotientMap ⇑h

Alias of Homeomorph.isQuotientMap.

theorem Homeomorph.coinduced_eq {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) : TopologicalSpace.coinduced (⇑h) inst✝¹ = inst✝

theorem Homeomorph.isEmbedding {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) : IsEmbedding ⇑h

@[deprecated Homeomorph.isEmbedding]

theorem Homeomorph.embedding {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) : IsEmbedding ⇑h

Alias of Homeomorph.isEmbedding.

noncomputable def Homeomorph.ofIsEmbedding {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) (hf : IsEmbedding f) : X ≃ₜ ↑(Set.range f)

Homeomorphism given an embedding.

Equations

• Homeomorph.ofIsEmbedding f hf = { toEquiv := Equiv.ofInjective f ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[deprecated Homeomorph.ofIsEmbedding]

def Homeomorph.ofEmbedding {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) (hf : IsEmbedding f) : X ≃ₜ ↑(Set.range f)

Alias of Homeomorph.ofIsEmbedding.

---

Homeomorphism given an embedding.

Equations

• @Homeomorph.ofEmbedding = @Homeomorph.ofIsEmbedding

theorem Homeomorph.secondCountableTopology {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [SecondCountableTopology Y] (h : X ≃ₜ Y) : SecondCountableTopology X

@[simp]

theorem Homeomorph.isCompact_image {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {s : Set X} (h : X ≃ₜ Y) : IsCompact (⇑h '' s) ↔ IsCompact s

If h : X → Y is a homeomorphism, h(s) is compact iff s is.

@[simp]

theorem Homeomorph.isCompact_preimage {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {s : Set Y} (h : X ≃ₜ Y) : IsCompact (⇑h ⁻¹' s) ↔ IsCompact s

If h : X → Y is a homeomorphism, h⁻¹(s) is compact iff s is.

@[simp]

theorem Homeomorph.isSigmaCompact_image {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {s : Set X} (h : X ≃ₜ Y) : IsSigmaCompact (⇑h '' s) ↔ IsSigmaCompact s

If h : X → Y is a homeomorphism, s is σ-compact iff h(s) is.

@[simp]

theorem Homeomorph.isSigmaCompact_preimage {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {s : Set Y} (h : X ≃ₜ Y) : IsSigmaCompact (⇑h ⁻¹' s) ↔ IsSigmaCompact s

If h : X → Y is a homeomorphism, h⁻¹(s) is σ-compact iff s is.

@[simp]

theorem Homeomorph.isPreconnected_image {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {s : Set X} (h : X ≃ₜ Y) : IsPreconnected (⇑h '' s) ↔ IsPreconnected s

@[simp]

theorem Homeomorph.isPreconnected_preimage {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {s : Set Y} (h : X ≃ₜ Y) : IsPreconnected (⇑h ⁻¹' s) ↔ IsPreconnected s

@[simp]

theorem Homeomorph.isConnected_image {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {s : Set X} (h : X ≃ₜ Y) : IsConnected (⇑h '' s) ↔ IsConnected s

@[simp]

theorem Homeomorph.isConnected_preimage {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {s : Set Y} (h : X ≃ₜ Y) : IsConnected (⇑h ⁻¹' s) ↔ IsConnected s

theorem Homeomorph.image_connectedComponentIn {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {s : Set X} (h : X ≃ₜ Y) {x : X} (hx : x ∈ s) : ⇑h '' connectedComponentIn s x = connectedComponentIn (⇑h '' s) (h x)

@[simp]

theorem Homeomorph.comap_cocompact {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) : Filter.comap (⇑h) (Filter.cocompact Y) = Filter.cocompact X

@[simp]

theorem Homeomorph.map_cocompact {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) : Filter.map (⇑h) (Filter.cocompact X) = Filter.cocompact Y

theorem Homeomorph.compactSpace {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [CompactSpace X] (h : X ≃ₜ Y) : CompactSpace Y

theorem Homeomorph.t0Space {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T0Space X] (h : X ≃ₜ Y) : T0Space Y

theorem Homeomorph.t1Space {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T1Space X] (h : X ≃ₜ Y) : T1Space Y

theorem Homeomorph.t2Space {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T2Space X] (h : X ≃ₜ Y) : T2Space Y

theorem Homeomorph.t25Space {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T25Space X] (h : X ≃ₜ Y) : T25Space Y

theorem Homeomorph.t3Space {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T3Space X] (h : X ≃ₜ Y) : T3Space Y

theorem Homeomorph.isDenseEmbedding {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) : IsDenseEmbedding ⇑h

@[deprecated Homeomorph.isDenseEmbedding]

theorem Homeomorph.denseEmbedding {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) : IsDenseEmbedding ⇑h

Alias of Homeomorph.isDenseEmbedding.

@[simp]

theorem Homeomorph.isOpen_preimage {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) {s : Set Y} : IsOpen (⇑h ⁻¹' s) ↔ IsOpen s

@[simp]

theorem Homeomorph.isOpen_image {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) {s : Set X} : IsOpen (⇑h '' s) ↔ IsOpen s

theorem Homeomorph.isOpenMap {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) : IsOpenMap ⇑h

@[simp]

theorem Homeomorph.isClosed_preimage {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) {s : Set Y} : IsClosed (⇑h ⁻¹' s) ↔ IsClosed s

@[simp]

theorem Homeomorph.isClosed_image {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) {s : Set X} : IsClosed (⇑h '' s) ↔ IsClosed s

theorem Homeomorph.isClosedMap {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) : IsClosedMap ⇑h

theorem Homeomorph.isOpenEmbedding {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) : IsOpenEmbedding ⇑h

@[deprecated Homeomorph.isOpenEmbedding]

theorem Homeomorph.openEmbedding {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) : IsOpenEmbedding ⇑h

Alias of Homeomorph.isOpenEmbedding.

theorem Homeomorph.isClosedEmbedding {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) : IsClosedEmbedding ⇑h

@[deprecated Homeomorph.isClosedEmbedding]

theorem Homeomorph.closedEmbedding {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) : IsClosedEmbedding ⇑h

Alias of Homeomorph.isClosedEmbedding.

theorem Homeomorph.normalSpace {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [NormalSpace X] (h : X ≃ₜ Y) : NormalSpace Y

theorem Homeomorph.t4Space {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T4Space X] (h : X ≃ₜ Y) : T4Space Y

theorem Homeomorph.t5Space {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T5Space X] (h : X ≃ₜ Y) : T5Space Y

theorem Homeomorph.preimage_closure {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) (s : Set Y) : ⇑h ⁻¹' closure s = closure (⇑h ⁻¹' s)

theorem Homeomorph.image_closure {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) (s : Set X) : ⇑h '' closure s = closure (⇑h '' s)

theorem Homeomorph.preimage_interior {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) (s : Set Y) : ⇑h ⁻¹' interior s = interior (⇑h ⁻¹' s)

theorem Homeomorph.image_interior {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) (s : Set X) : ⇑h '' interior s = interior (⇑h '' s)

theorem Homeomorph.preimage_frontier {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) (s : Set Y) : ⇑h ⁻¹' frontier s = frontier (⇑h ⁻¹' s)

theorem Homeomorph.image_frontier {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) (s : Set X) : ⇑h '' frontier s = frontier (⇑h '' s)

theorem HasCompactMulSupport.comp_homeomorph {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {M : Type u_7} [One M] {f : Y → M} (hf : HasCompactMulSupport f) (φ : X ≃ₜ Y) : HasCompactMulSupport (f ∘ ⇑φ)

theorem HasCompactSupport.comp_homeomorph {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {M : Type u_7} [Zero M] {f : Y → M} (hf : HasCompactSupport f) (φ : X ≃ₜ Y) : HasCompactSupport (f ∘ ⇑φ)

@[simp]

theorem Homeomorph.map_nhds_eq {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) (x : X) : Filter.map (⇑h) (nhds x) = nhds (h x)

@[simp]

theorem Homeomorph.map_punctured_nhds_eq {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) (x : X) : Filter.map (⇑h) (nhdsWithin x {x}ᶜ) = nhdsWithin (h x) {h x}ᶜ

theorem Homeomorph.symm_map_nhds_eq {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) (x : X) : Filter.map (⇑h.symm) (nhds (h x)) = nhds x

theorem Homeomorph.nhds_eq_comap {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) (x : X) : nhds x = Filter.comap (⇑h) (nhds (h x))

@[simp]

theorem Homeomorph.comap_nhds_eq {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) (y : Y) : Filter.comap (⇑h) (nhds y) = nhds (h.symm y)

@[simp]

theorem Homeomorph.comap_coclosedCompact {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) : Filter.comap (⇑h) (Filter.coclosedCompact Y) = Filter.coclosedCompact X

@[simp]

theorem Homeomorph.map_coclosedCompact {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) : Filter.map (⇑h) (Filter.coclosedCompact X) = Filter.coclosedCompact Y

theorem Homeomorph.locallyConnectedSpace {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [i : LocallyConnectedSpace Y] (h : X ≃ₜ Y) : LocallyConnectedSpace X

If the codomain of a homeomorphism is a locally connected space, then the domain is also a locally connected space.

theorem Homeomorph.locallyCompactSpace_iff {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) : LocallyCompactSpace X ↔ LocallyCompactSpace Y

The codomain of a homeomorphism is a locally compact space if and only if the domain is a locally compact space.

def Homeomorph.homeomorphOfContinuousOpen {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : X ≃ Y) (h₁ : Continuous ⇑e) (h₂ : IsOpenMap ⇑e) : X ≃ₜ Y

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 := ⋯ }

@[simp]

theorem Homeomorph.homeomorphOfContinuousOpen_toEquiv {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : X ≃ Y) (h₁ : Continuous ⇑e) (h₂ : IsOpenMap ⇑e) : (Homeomorph.homeomorphOfContinuousOpen e h₁ h₂).toEquiv = e

def Homeomorph.homeomorphOfContinuousClosed {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : X ≃ Y) (h₁ : Continuous ⇑e) (h₂ : IsClosedMap ⇑e) : X ≃ₜ Y

If a bijective map e : X ≃ Y is continuous and closed, then it is a homeomorphism.

Equations

• Homeomorph.homeomorphOfContinuousClosed e h₁ h₂ = { toEquiv := e, continuous_toFun := h₁, continuous_invFun := ⋯ }

@[simp]

theorem Homeomorph.homeomorphOfContinuousOpen_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : X ≃ Y) (h₁ : Continuous ⇑e) (h₂ : IsOpenMap ⇑e) : ⇑(Homeomorph.homeomorphOfContinuousOpen e h₁ h₂) = ⇑e

@[simp]

theorem Homeomorph.homeomorphOfContinuousOpen_symm_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : X ≃ Y) (h₁ : Continuous ⇑e) (h₂ : IsOpenMap ⇑e) : ⇑(Homeomorph.homeomorphOfContinuousOpen e h₁ h₂).symm = ⇑e.symm

@[simp]

theorem Homeomorph.comp_continuousOn_iff {X : Type u_1} {Y : Type u_2} {Z : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (h : X ≃ₜ Y) (f : Z → X) (s : Set Z) : ContinuousOn (⇑h ∘ f) s ↔ ContinuousOn f s

@[simp]

theorem Homeomorph.comp_continuous_iff {X : Type u_1} {Y : Type u_2} {Z : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (h : X ≃ₜ Y) {f : Z → X} : Continuous (⇑h ∘ f) ↔ Continuous f

@[simp]

theorem Homeomorph.comp_continuous_iff' {X : Type u_1} {Y : Type u_2} {Z : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (h : X ≃ₜ Y) {f : Y → Z} : Continuous (f ∘ ⇑h) ↔ Continuous f

theorem Homeomorph.comp_continuousAt_iff {X : Type u_1} {Y : Type u_2} {Z : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (h : X ≃ₜ Y) (f : Z → X) (z : Z) : ContinuousAt (⇑h ∘ f) z ↔ ContinuousAt f z

theorem Homeomorph.comp_continuousAt_iff' {X : Type u_1} {Y : Type u_2} {Z : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (h : X ≃ₜ Y) (f : Y → Z) (x : X) : ContinuousAt (f ∘ ⇑h) x ↔ ContinuousAt f (h x)

theorem Homeomorph.comp_continuousWithinAt_iff {X : Type u_1} {Y : Type u_2} {Z : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (h : X ≃ₜ Y) (f : Z → X) (s : Set Z) (z : Z) : ContinuousWithinAt f s z ↔ ContinuousWithinAt (⇑h ∘ f) s z

@[simp]

theorem Homeomorph.comp_isOpenMap_iff {X : Type u_1} {Y : Type u_2} {Z : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (h : X ≃ₜ Y) {f : Z → X} : IsOpenMap (⇑h ∘ f) ↔ IsOpenMap f

@[simp]

theorem Homeomorph.comp_isOpenMap_iff' {X : Type u_1} {Y : Type u_2} {Z : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (h : X ≃ₜ Y) {f : Y → Z} : IsOpenMap (f ∘ ⇑h) ↔ IsOpenMap f

def Homeomorph.subtype {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {p : X → Prop} {q : Y → Prop} (h : X ≃ₜ Y) (h_iff : ∀ (x : X), p x ↔ q (h x)) : { x : X // p x } ≃ₜ { y : Y // q y }

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 := ⋯ }

@[simp]

theorem Homeomorph.subtype_apply_coe {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {p : X → Prop} {q : Y → Prop} (h : X ≃ₜ Y) (h_iff : ∀ (x : X), p x ↔ q (h x)) (a : { a : X // p a }) : ↑((h.subtype h_iff) a) = h ↑a

@[simp]

theorem Homeomorph.subtype_symm_apply_coe {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {p : X → Prop} {q : Y → Prop} (h : X ≃ₜ Y) (h_iff : ∀ (x : X), p x ↔ q (h x)) (b : { b : Y // q b }) : ↑((h.subtype h_iff).symm b) = h.symm ↑b

@[simp]

theorem Homeomorph.subtype_toEquiv {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {p : X → Prop} {q : Y → Prop} (h : X ≃ₜ Y) (h_iff : ∀ (x : X), p x ↔ q (h x)) : (h.subtype h_iff).toEquiv = h.subtypeEquiv h_iff

@[reducible, inline]

abbrev Homeomorph.sets {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {s : Set X} {t : Set Y} (h : X ≃ₜ Y) (h_eq : s = ⇑h ⁻¹' t) : ↑s ≃ₜ ↑t

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 ⋯

def Homeomorph.setCongr {X : Type u_1} [TopologicalSpace X] {s : Set X} {t : Set X} (h : s = t) : ↑s ≃ₜ ↑t

If two sets are equal, then they are homeomorphic.

Equations

• Homeomorph.setCongr h = { toEquiv := Equiv.setCongr h, continuous_toFun := ⋯, continuous_invFun := ⋯ }

def Homeomorph.sumCongr {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {X' : Type u_5} {Y' : Type u_6} [TopologicalSpace X'] [TopologicalSpace Y'] (h₁ : X ≃ₜ X') (h₂ : Y ≃ₜ Y') : X ⊕ Y ≃ₜ X' ⊕ Y'

Sum of two homeomorphisms.

Equations

• h₁.sumCongr h₂ = { toEquiv := h₁.sumCongr h₂.toEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }

def Homeomorph.prodCongr {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {X' : Type u_5} {Y' : Type u_6} [TopologicalSpace X'] [TopologicalSpace Y'] (h₁ : X ≃ₜ X') (h₂ : Y ≃ₜ Y') : X × Y ≃ₜ X' × Y'

Product of two homeomorphisms.

Equations

• h₁.prodCongr h₂ = { toEquiv := h₁.prodCongr h₂.toEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem Homeomorph.prodCongr_symm {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {X' : Type u_5} {Y' : Type u_6} [TopologicalSpace X'] [TopologicalSpace Y'] (h₁ : X ≃ₜ X') (h₂ : Y ≃ₜ Y') : (h₁.prodCongr h₂).symm = h₁.symm.prodCongr h₂.symm

@[simp]

theorem Homeomorph.coe_prodCongr {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {X' : Type u_5} {Y' : Type u_6} [TopologicalSpace X'] [TopologicalSpace Y'] (h₁ : X ≃ₜ X') (h₂ : Y ≃ₜ Y') : ⇑(h₁.prodCongr h₂) = Prod.map ⇑h₁ ⇑h₂

def Homeomorph.sumComm (X : Type u_1) (Y : Type u_2) [TopologicalSpace X] [TopologicalSpace Y] : X ⊕ Y ≃ₜ Y ⊕ X

X ⊕ Y is homeomorphic to Y ⊕ X.

Equations

• Homeomorph.sumComm X Y = { toEquiv := Equiv.sumComm X Y, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem Homeomorph.sumComm_symm (X : Type u_1) (Y : Type u_2) [TopologicalSpace X] [TopologicalSpace Y] : (Homeomorph.sumComm X Y).symm = Homeomorph.sumComm Y X

@[simp]

theorem Homeomorph.coe_sumComm (X : Type u_1) (Y : Type u_2) [TopologicalSpace X] [TopologicalSpace Y] : ⇑(Homeomorph.sumComm X Y) = Sum.swap

theorem Homeomorph.continuous_sumAssoc (X : Type u_1) (Y : Type u_2) (Z : Type u_4) [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] : Continuous ⇑(Equiv.sumAssoc X Y Z)

theorem Homeomorph.continuous_sumAssoc_symm (X : Type u_1) (Y : Type u_2) (Z : Type u_4) [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] : Continuous ⇑(Equiv.sumAssoc X Y Z).symm

def Homeomorph.sumAssoc (X : Type u_1) (Y : Type u_2) (Z : Type u_4) [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] : (X ⊕ Y) ⊕ Z ≃ₜ X ⊕ Y ⊕ Z

(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 := ⋯ }

@[simp]

theorem Homeomorph.sumAssoc_toEquiv (X : Type u_1) (Y : Type u_2) (Z : Type u_4) [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] : (Homeomorph.sumAssoc X Y Z).toEquiv = Equiv.sumAssoc X Y Z

def Homeomorph.sumSumSumComm (X : Type u_1) (Y : Type u_2) (W : Type u_3) (Z : Type u_4) [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace W] [TopologicalSpace Z] : (X ⊕ Y) ⊕ W ⊕ Z ≃ₜ (X ⊕ W) ⊕ Y ⊕ Z

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 := ⋯ }

@[simp]

theorem Homeomorph.sumSumSumComm_toEquiv (X : Type u_1) (Y : Type u_2) (W : Type u_3) (Z : Type u_4) [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace W] [TopologicalSpace Z] : (Homeomorph.sumSumSumComm X Y W Z).toEquiv = Equiv.sumSumSumComm X Y W Z

@[simp]

theorem Homeomorph.sumSumSumComm_symm (X : Type u_1) (Y : Type u_2) (W : Type u_3) (Z : Type u_4) [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace W] [TopologicalSpace Z] : (Homeomorph.sumSumSumComm X Y W Z).symm = Homeomorph.sumSumSumComm X W Y Z

def Homeomorph.sumEmpty (X : Type u_1) (Y : Type u_2) [TopologicalSpace X] [TopologicalSpace Y] [IsEmpty Y] : X ⊕ Y ≃ₜ X

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 := ⋯ }

@[simp]

theorem Homeomorph.sumEmpty_apply (X : Type u_1) (Y : Type u_2) [TopologicalSpace X] [TopologicalSpace Y] [IsEmpty Y] : ⇑(Homeomorph.sumEmpty X Y) = Sum.elim id fun (a : Y) => isEmptyElim a

def Homeomorph.emptySum (X : Type u_1) (Y : Type u_2) [TopologicalSpace X] [TopologicalSpace Y] [IsEmpty Y] : Y ⊕ X ≃ₜ X

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)

@[simp]

theorem Homeomorph.coe_emptySum (X : Type u_1) (Y : Type u_2) [TopologicalSpace X] [TopologicalSpace Y] [IsEmpty Y] : (Homeomorph.emptySum X Y).toEquiv = Equiv.emptySum Y X

def Homeomorph.prodComm (X : Type u_1) (Y : Type u_2) [TopologicalSpace X] [TopologicalSpace Y] : X × Y ≃ₜ Y × X

X × Y is homeomorphic to Y × X.

Equations

• Homeomorph.prodComm X Y = { toEquiv := Equiv.prodComm X Y, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem Homeomorph.prodComm_symm (X : Type u_1) (Y : Type u_2) [TopologicalSpace X] [TopologicalSpace Y] : (Homeomorph.prodComm X Y).symm = Homeomorph.prodComm Y X

@[simp]

theorem Homeomorph.coe_prodComm (X : Type u_1) (Y : Type u_2) [TopologicalSpace X] [TopologicalSpace Y] : ⇑(Homeomorph.prodComm X Y) = Prod.swap

def Homeomorph.prodAssoc (X : Type u_1) (Y : Type u_2) (Z : Type u_4) [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] : (X × Y) × Z ≃ₜ X × Y × Z

(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 := ⋯ }

@[simp]

theorem Homeomorph.prodAssoc_toEquiv (X : Type u_1) (Y : Type u_2) (Z : Type u_4) [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] : (Homeomorph.prodAssoc X Y Z).toEquiv = Equiv.prodAssoc X Y Z

def Homeomorph.prodProdProdComm (X : Type u_1) (Y : Type u_2) (W : Type u_3) (Z : Type u_4) [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace W] [TopologicalSpace Z] : (X × Y) × W × Z ≃ₜ (X × W) × Y × Z

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 := ⋯ }

@[simp]

theorem Homeomorph.prodProdProdComm_symm (X : Type u_1) (Y : Type u_2) (W : Type u_3) (Z : Type u_4) [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace W] [TopologicalSpace Z] : (Homeomorph.prodProdProdComm X Y W Z).symm = Homeomorph.prodProdProdComm X W Y Z

def Homeomorph.prodPUnit (X : Type u_1) [TopologicalSpace X] : X × PUnit.{u_7 + 1} ≃ₜ X

X × {*} is homeomorphic to X.

Equations

• Homeomorph.prodPUnit X = { toEquiv := Equiv.prodPUnit X, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem Homeomorph.prodPUnit_apply (X : Type u_1) [TopologicalSpace X] : ⇑(Homeomorph.prodPUnit X) = fun (p : X × PUnit.{u_7 + 1} ) => p.1

def Homeomorph.punitProd (X : Type u_1) [TopologicalSpace X] : PUnit.{u_7 + 1} × X ≃ₜ X

{*} × X is homeomorphic to X.

Equations

• Homeomorph.punitProd X = (Homeomorph.prodComm PUnit.{?u.15 + 1} X).trans (Homeomorph.prodPUnit X)

@[simp]

theorem Homeomorph.coe_punitProd (X : Type u_1) [TopologicalSpace X] : ⇑(Homeomorph.punitProd X) = Prod.snd

def Homeomorph.homeomorphOfUnique (X : Type u_1) (Y : Type u_2) [TopologicalSpace X] [TopologicalSpace Y] [Unique X] [Unique Y] : X ≃ₜ Y

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 := ⋯ }

@[simp]

theorem Homeomorph.homeomorphOfUnique_symm_apply (X : Type u_1) (Y : Type u_2) [TopologicalSpace X] [TopologicalSpace Y] [Unique X] [Unique Y] : ∀ (a : Y), (Homeomorph.homeomorphOfUnique X Y).symm a = default

@[simp]

theorem Homeomorph.homeomorphOfUnique_apply (X : Type u_1) (Y : Type u_2) [TopologicalSpace X] [TopologicalSpace Y] [Unique X] [Unique Y] : ∀ (a : X), (Homeomorph.homeomorphOfUnique X Y) a = default

def Homeomorph.piCongrLeft {ι : Type u_7} {ι' : Type u_8} {Y : ι' → Type u_9} [(j : ι') → TopologicalSpace (Y j)] (e : ι ≃ ι') : ((i : ι) → Y (e i)) ≃ₜ ((j : ι') → Y j)

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 := ⋯ }

@[simp]

theorem Homeomorph.piCongrLeft_apply {ι : Type u_7} {ι' : Type u_8} {Y : ι' → Type u_9} [(j : ι') → TopologicalSpace (Y j)] (e : ι ≃ ι') : ∀ (a : (b : ι) → Y (e.symm.symm b)) (a_1 : ι'), (Homeomorph.piCongrLeft e) a a_1 = (Equiv.piCongrLeft' Y e.symm).symm a a_1

@[simp]

theorem Homeomorph.piCongrLeft_toEquiv {ι : Type u_7} {ι' : Type u_8} {Y : ι' → Type u_9} [(j : ι') → TopologicalSpace (Y j)] (e : ι ≃ ι') : (Homeomorph.piCongrLeft e).toEquiv = Equiv.piCongrLeft Y e

def Homeomorph.piCongrRight {ι : Type u_7} {Y₁ : ι → Type u_8} {Y₂ : ι → Type u_9} [(i : ι) → TopologicalSpace (Y₁ i)] [(i : ι) → TopologicalSpace (Y₂ i)] (F : (i : ι) → Y₁ i ≃ₜ Y₂ i) : ((i : ι) → Y₁ i) ≃ₜ ((i : ι) → Y₂ i)

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 := ⋯ }

@[simp]

theorem Homeomorph.piCongrRight_apply {ι : Type u_7} {Y₁ : ι → Type u_8} {Y₂ : ι → Type u_9} [(i : ι) → TopologicalSpace (Y₁ i)] [(i : ι) → TopologicalSpace (Y₂ i)] (F : (i : ι) → Y₁ i ≃ₜ Y₂ i) : ∀ (a : (i : ι) → Y₁ i) (i : ι), (Homeomorph.piCongrRight F) a i = (F i) (a i)

@[simp]

theorem Homeomorph.piCongrRight_toEquiv {ι : Type u_7} {Y₁ : ι → Type u_8} {Y₂ : ι → Type u_9} [(i : ι) → TopologicalSpace (Y₁ i)] [(i : ι) → TopologicalSpace (Y₂ i)] (F : (i : ι) → Y₁ i ≃ₜ Y₂ i) : (Homeomorph.piCongrRight F).toEquiv = Equiv.piCongrRight fun (i : ι) => (F i).toEquiv

@[simp]

theorem Homeomorph.piCongrRight_symm {ι : Type u_7} {Y₁ : ι → Type u_8} {Y₂ : ι → Type u_9} [(i : ι) → TopologicalSpace (Y₁ i)] [(i : ι) → TopologicalSpace (Y₂ i)] (F : (i : ι) → Y₁ i ≃ₜ Y₂ i) : (Homeomorph.piCongrRight F).symm = Homeomorph.piCongrRight fun (i : ι) => (F i).symm

def Homeomorph.piCongr {ι₁ : Type u_7} {ι₂ : Type u_8} {Y₁ : ι₁ → Type u_9} {Y₂ : ι₂ → Type u_10} [(i₁ : ι₁) → TopologicalSpace (Y₁ i₁)] [(i₂ : ι₂) → TopologicalSpace (Y₂ i₂)] (e : ι₁ ≃ ι₂) (F : (i₁ : ι₁) → Y₁ i₁ ≃ₜ Y₂ (e i₁)) : ((i₁ : ι₁) → Y₁ i₁) ≃ₜ ((i₂ : ι₂) → Y₂ i₂)

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)

@[simp]

theorem Homeomorph.piCongr_apply {ι₁ : Type u_7} {ι₂ : Type u_8} {Y₁ : ι₁ → Type u_9} {Y₂ : ι₂ → Type u_10} [(i₁ : ι₁) → TopologicalSpace (Y₁ i₁)] [(i₂ : ι₂) → TopologicalSpace (Y₂ i₂)] (e : ι₁ ≃ ι₂) (F : (i₁ : ι₁) → Y₁ i₁ ≃ₜ Y₂ (e i₁)) : ∀ (a : (i : ι₁) → Y₁ i) (i₂ : ι₂), (Homeomorph.piCongr e F) a i₂ = ⋯ ▸ (Equiv.piCongrRight fun (i : ι₁) => (F i).toEquiv) a (e.symm i₂)

@[simp]

theorem Homeomorph.piCongr_toEquiv {ι₁ : Type u_7} {ι₂ : Type u_8} {Y₁ : ι₁ → Type u_9} {Y₂ : ι₂ → Type u_10} [(i₁ : ι₁) → TopologicalSpace (Y₁ i₁)] [(i₂ : ι₂) → TopologicalSpace (Y₂ i₂)] (e : ι₁ ≃ ι₂) (F : (i₁ : ι₁) → Y₁ i₁ ≃ₜ Y₂ (e i₁)) : (Homeomorph.piCongr e F).toEquiv = (Equiv.piCongrRight fun (i : ι₁) => (F i).toEquiv).trans (Equiv.piCongrLeft Y₂ e)

def Homeomorph.ulift {X : Type u} [TopologicalSpace X] : ULift.{v, u} X ≃ₜ X

ULift X is homeomorphic to X.

Equations

• Homeomorph.ulift = { toEquiv := Equiv.ulift, continuous_toFun := ⋯, continuous_invFun := ⋯ }

def Homeomorph.sumArrowHomeomorphProdArrow {X : Type u_1} [TopologicalSpace X] {ι : Type u_7} {ι' : Type u_8} : (ι ⊕ ι' → X) ≃ₜ (ι → X) × (ι' → X)

The natural homeomorphism (ι ⊕ ι' → X) ≃ₜ (ι → X) × (ι' → X). Equiv.sumArrowEquivProdArrow as a homeomorphism.

Equations

• Homeomorph.sumArrowHomeomorphProdArrow = { toEquiv := Equiv.sumArrowEquivProdArrow ι ι' X, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem Homeomorph.sumArrowHomeomorphProdArrow_apply {X : Type u_1} [TopologicalSpace X] {ι : Type u_7} {ι' : Type u_8} (f : ι ⊕ ι' → X) : Homeomorph.sumArrowHomeomorphProdArrow f = (f ∘ Sum.inl, f ∘ Sum.inr)

@[simp]

theorem Homeomorph.sumArrowHomeomorphProdArrow_symm_apply {X : Type u_1} [TopologicalSpace X] {ι : Type u_7} {ι' : Type u_8} (p : (ι → X) × (ι' → X)) : ∀ (a : ι ⊕ ι'), Homeomorph.sumArrowHomeomorphProdArrow.symm p a = Sum.elim p.1 p.2 a

theorem Fin.continuous_append {X : Type u_1} [TopologicalSpace X] (m : ℕ) (n : ℕ) : Continuous fun (p : (Fin m → X) × (Fin n → X)) => Fin.append p.1 p.2

def Fin.appendHomeomorph {X : Type u_1} [TopologicalSpace X] (m : ℕ) (n : ℕ) : (Fin m → X) × (Fin n → X) ≃ₜ (Fin (m + n) → X)

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 := ⋯ }

@[simp]

theorem Fin.appendHomeomorph_symm_apply {X : Type u_1} [TopologicalSpace X] (m : ℕ) (n : ℕ) (f : Fin (m + n) → X) : (Fin.appendHomeomorph m n).symm f = (fun (i : Fin m) => f (Fin.castAdd n i), fun (i : Fin n) => f (Fin.natAdd m i))

@[simp]

theorem Fin.appendHomeomorph_apply {X : Type u_1} [TopologicalSpace X] (m : ℕ) (n : ℕ) (fg : (Fin m → X) × (Fin n → X)) : ∀ (a : Fin (m + n)), (Fin.appendHomeomorph m n) fg a = Fin.append fg.1 fg.2 a

@[simp]

theorem Fin.appendHomeomorph_toEquiv {X : Type u_1} [TopologicalSpace X] (m : ℕ) (n : ℕ) : (Fin.appendHomeomorph m n).toEquiv = Fin.appendEquiv m n

def Homeomorph.sumProdDistrib {X : Type u_1} {Y : Type u_2} {Z : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] : (X ⊕ Y) × Z ≃ₜ X × Z ⊕ Y × Z

(X ⊕ Y) × Z is homeomorphic to X × Z ⊕ Y × Z.

Equations

• Homeomorph.sumProdDistrib = (Homeomorph.homeomorphOfContinuousOpen (Equiv.sumProdDistrib X Y Z).symm ⋯ ⋯).symm

@[simp]

theorem Homeomorph.sumProdDistrib_apply {X : Type u_1} {Y : Type u_2} {Z : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] : ∀ (a : (X ⊕ Y) × Z), Homeomorph.sumProdDistrib a = (Equiv.sumProdDistrib X Y Z) a

@[simp]

theorem Homeomorph.sumProdDistrib_symm_apply {X : Type u_1} {Y : Type u_2} {Z : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] : ∀ (a : X × Z ⊕ Y × Z), Homeomorph.sumProdDistrib.symm a = (Equiv.sumProdDistrib X Y Z).symm a

def Homeomorph.prodSumDistrib {X : Type u_1} {Y : Type u_2} {Z : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] : X × (Y ⊕ Z) ≃ₜ X × Y ⊕ X × Z

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)))

def Homeomorph.sigmaProdDistrib {Y : Type u_2} [TopologicalSpace Y] {ι : Type u_7} {X : ι → Type u_8} [(i : ι) → TopologicalSpace (X i)] : ((i : ι) × X i) × Y ≃ₜ (i : ι) × X i × Y

(Σ i, X i) × Y is homeomorphic to Σ i, (X i × Y).

Equations

• Homeomorph.sigmaProdDistrib = (Homeomorph.homeomorphOfContinuousOpen (Equiv.sigmaProdDistrib X Y).symm ⋯ ⋯).symm

@[simp]

theorem Homeomorph.sigmaProdDistrib_apply {Y : Type u_2} [TopologicalSpace Y] {ι : Type u_7} {X : ι → Type u_8} [(i : ι) → TopologicalSpace (X i)] : ∀ (a : ((i : ι) × X i) × Y), Homeomorph.sigmaProdDistrib a = ⟨a.1.fst, (a.1.snd, a.2)⟩

@[simp]

theorem Homeomorph.sigmaProdDistrib_symm_apply {Y : Type u_2} [TopologicalSpace Y] {ι : Type u_7} {X : ι → Type u_8} [(i : ι) → TopologicalSpace (X i)] : ∀ (a : (i : ι) × X i × Y), Homeomorph.sigmaProdDistrib.symm a = (⟨a.fst, a.snd.1⟩, a.snd.2)

@[simp]

theorem Homeomorph.sigmaProdDistrib_toEquiv {Y : Type u_2} [TopologicalSpace Y] {ι : Type u_7} {X : ι → Type u_8} [(i : ι) → TopologicalSpace (X i)] : Homeomorph.sigmaProdDistrib.toEquiv = Equiv.sigmaProdDistrib X Y

def Homeomorph.funUnique (ι : Type u_7) (X : Type u_8) [Unique ι] [TopologicalSpace X] : (ι → X) ≃ₜ X

If ι has a unique element, then ι → X is homeomorphic to X.

Equations

• Homeomorph.funUnique ι X = { toEquiv := Equiv.funUnique ι X, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem Homeomorph.funUnique_apply (ι : Type u_7) (X : Type u_8) [Unique ι] [TopologicalSpace X] : ⇑(Homeomorph.funUnique ι X) = fun (f : ι → X) => f default

@[simp]

theorem Homeomorph.funUnique_symm_apply (ι : Type u_7) (X : Type u_8) [Unique ι] [TopologicalSpace X] : ⇑(Homeomorph.funUnique ι X).symm = uniqueElim

def Homeomorph.piFinTwo (X : Fin 2 → Type u) [(i : Fin 2) → TopologicalSpace (X i)] : ((i : Fin 2) → X i) ≃ₜ X 0 × X 1

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 := ⋯ }

@[simp]

theorem Homeomorph.piFinTwo_apply (X : Fin 2 → Type u) [(i : Fin 2) → TopologicalSpace (X i)] : ⇑(Homeomorph.piFinTwo X) = fun (f : (i : Fin 2) → X i) => (f 0, f 1)

@[simp]

theorem Homeomorph.piFinTwo_symm_apply (X : Fin 2 → Type u) [(i : Fin 2) → TopologicalSpace (X i)] : ⇑(Homeomorph.piFinTwo X).symm = fun (p : X 0 × X 1) => Fin.cons p.1 (Fin.cons p.2 finZeroElim)

def Homeomorph.finTwoArrow {X : Type u_1} [TopologicalSpace X] : (Fin 2 → X) ≃ₜ X × X

Homeomorphism between X² = Fin 2 → X and X × X.

Equations

• Homeomorph.finTwoArrow = { toEquiv := finTwoArrowEquiv X, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem Homeomorph.finTwoArrow_apply {X : Type u_1} [TopologicalSpace X] : ⇑Homeomorph.finTwoArrow = fun (f : Fin 2 → X) => (f 0, f 1)

@[simp]

theorem Homeomorph.finTwoArrow_symm_apply {X : Type u_1} [TopologicalSpace X] : ⇑Homeomorph.finTwoArrow.symm = fun (x : X × X) => ![x.1, x.2]

def Homeomorph.image {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : X ≃ₜ Y) (s : Set X) : ↑s ≃ₜ ↑(⇑e '' s)

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 := ⋯ }

@[simp]

theorem Homeomorph.image_apply_coe {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : X ≃ₜ Y) (s : Set X) (x : ↑s) : ↑((e.image s) x) = e ↑x

@[simp]

theorem Homeomorph.image_symm_apply_coe {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : X ≃ₜ Y) (s : Set X) (y : ↑(⇑e.toEquiv '' s)) : ↑((e.image s).symm y) = e.symm ↑y

def Homeomorph.Set.univ (X : Type u_7) [TopologicalSpace X] : ↑Set.univ ≃ₜ X

Set.univ X is homeomorphic to X.

Equations

• Homeomorph.Set.univ X = { toEquiv := Equiv.Set.univ X, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem Homeomorph.Set.univ_symm_apply_coe (X : Type u_7) [TopologicalSpace X] (a : X) : ↑((Homeomorph.Set.univ X).symm a) = a

@[simp]

theorem Homeomorph.Set.univ_apply (X : Type u_7) [TopologicalSpace X] : ⇑(Homeomorph.Set.univ X) = Subtype.val

def Homeomorph.Set.prod {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (s : Set X) (t : Set Y) : ↑(s ×ˢ t) ≃ₜ ↑s × ↑t

s ×ˢ t is homeomorphic to s × t.

Equations

• Homeomorph.Set.prod s t = { toEquiv := Equiv.Set.prod s t, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem Homeomorph.Set.prod_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (s : Set X) (t : Set Y) (x : { c : X × Y // s c.1 ∧ t c.2 }) : (Homeomorph.Set.prod s t) x = (⟨(↑x).1, ⋯⟩, ⟨(↑x).2, ⋯⟩)

@[simp]

theorem Homeomorph.Set.prod_symm_apply_coe {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (s : Set X) (t : Set Y) (x : { a : X // s a } × { b : Y // t b }) : ↑((Homeomorph.Set.prod s t).symm x) = (↑x.1, ↑x.2)

def Homeomorph.piEquivPiSubtypeProd {ι : Type u_7} (p : ι → Prop) (Y : ι → Type u_8) [(i : ι) → TopologicalSpace (Y i)] [DecidablePred p] : ((i : ι) → Y i) ≃ₜ ((i : { x : ι // p x }) → Y ↑i) × ((i : { x : ι // ¬p x }) → Y ↑i)

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 := ⋯ }

@[simp]

theorem Homeomorph.piEquivPiSubtypeProd_symm_apply {ι : Type u_7} (p : ι → Prop) (Y : ι → Type u_8) [(i : ι) → TopologicalSpace (Y i)] [DecidablePred p] (f : ((i : { x : ι // p x }) → Y ↑i) × ((i : { x : ι // ¬p x }) → Y ↑i)) (x : ι) : (Homeomorph.piEquivPiSubtypeProd p Y).symm f x = if h : p x then f.1 ⟨x, h⟩ else f.2 ⟨x, h⟩

@[simp]

theorem Homeomorph.piEquivPiSubtypeProd_apply {ι : Type u_7} (p : ι → Prop) (Y : ι → Type u_8) [(i : ι) → TopologicalSpace (Y i)] [DecidablePred p] (f : (i : ι) → Y i) : (Homeomorph.piEquivPiSubtypeProd p Y) f = (fun (x : { x : ι // p x }) => f ↑x, fun (x : { x : ι // ¬p x }) => f ↑x)

def Homeomorph.piSplitAt {ι : Type u_7} [DecidableEq ι] (i : ι) (Y : ι → Type u_8) [(j : ι) → TopologicalSpace (Y j)] : ((j : ι) → Y j) ≃ₜ Y i × ((j : { j : ι // j ≠ i }) → Y ↑j)

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 := ⋯ }

@[simp]

theorem Homeomorph.piSplitAt_apply {ι : Type u_7} [DecidableEq ι] (i : ι) (Y : ι → Type u_8) [(j : ι) → TopologicalSpace (Y j)] (f : (j : ι) → Y j) : (Homeomorph.piSplitAt i Y) f = (f i, fun (j : { j : ι // ¬j = i }) => f ↑j)

@[simp]

theorem Homeomorph.piSplitAt_symm_apply {ι : Type u_7} [DecidableEq ι] (i : ι) (Y : ι → Type u_8) [(j : ι) → TopologicalSpace (Y j)] (f : Y i × ((j : { j : ι // j ≠ i }) → Y ↑j)) (j : ι) : (Homeomorph.piSplitAt i Y).symm f j = if h : j = i then ⋯ ▸ f.1 else f.2 ⟨j, h⟩

def Homeomorph.funSplitAt (Y : Type u_2) [TopologicalSpace Y] {ι : Type u_7} [DecidableEq ι] (i : ι) : (ι → Y) ≃ₜ Y × ({ j : ι // j ≠ i } → Y)

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

@[simp]

theorem Homeomorph.funSplitAt_symm_apply (Y : Type u_2) [TopologicalSpace Y] {ι : Type u_7} [DecidableEq ι] (i : ι) (f : (fun (a : ι) => Y) i × ((j : { j : ι // j ≠ i }) → (fun (a : ι) => Y) ↑j)) (j : ι) : (Homeomorph.funSplitAt Y i).symm f j = if h : j = i then f.1 else f.2 ⟨j, ⋯⟩

@[simp]

theorem Homeomorph.funSplitAt_apply (Y : Type u_2) [TopologicalSpace Y] {ι : Type u_7} [DecidableEq ι] (i : ι) (f : (j : ι) → (fun (a : ι) => Y) j) : (Homeomorph.funSplitAt Y i) f = (f i, fun (j : { j : ι // ¬j = i }) => f ↑j)

def Equiv.toHomeomorph {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : X ≃ Y) (he : ∀ (s : Set Y), IsOpen (⇑e ⁻¹' s) ↔ IsOpen s) : X ≃ₜ Y

An equiv between topological spaces respecting openness is a homeomorphism.

Equations

• e.toHomeomorph he = { toEquiv := e, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem Equiv.toHomeomorph_toEquiv {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : X ≃ Y) (he : ∀ (s : Set Y), IsOpen (⇑e ⁻¹' s) ↔ IsOpen s) : (e.toHomeomorph he).toEquiv = e

@[simp]

theorem Equiv.coe_toHomeomorph {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : X ≃ Y) (he : ∀ (s : Set Y), IsOpen (⇑e ⁻¹' s) ↔ IsOpen s) : ⇑(e.toHomeomorph he) = ⇑e

theorem Equiv.toHomeomorph_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : X ≃ Y) (he : ∀ (s : Set Y), IsOpen (⇑e ⁻¹' s) ↔ IsOpen s) (x : X) : (e.toHomeomorph he) x = e x

@[simp]

theorem Equiv.toHomeomorph_refl {X : Type u_1} [TopologicalSpace X] : (Equiv.refl X).toHomeomorph ⋯ = Homeomorph.refl X

@[simp]

theorem Equiv.toHomeomorph_symm {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : X ≃ Y) (he : ∀ (s : Set Y), IsOpen (⇑e ⁻¹' s) ↔ IsOpen s) : (e.toHomeomorph he).symm = e.symm.toHomeomorph ⋯

theorem Equiv.toHomeomorph_trans {X : Type u_1} {Y : Type u_2} {Z : Type u_5} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (e : X ≃ Y) (f : Y ≃ Z) (he : ∀ (s : Set Y), IsOpen (⇑e ⁻¹' s) ↔ IsOpen s) (hf : ∀ (s : Set Z), IsOpen (⇑f ⁻¹' s) ↔ IsOpen s) : (e.trans f).toHomeomorph ⋯ = (e.toHomeomorph he).trans (f.toHomeomorph hf)

def Equiv.toHomeomorphOfIsInducing {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X ≃ Y) (hf : IsInducing ⇑f) : X ≃ₜ Y

An inducing equiv between topological spaces is a homeomorphism.

Equations

• f.toHomeomorphOfIsInducing hf = { toEquiv := f, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem Equiv.toHomeomorphOfIsInducing_toEquiv {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X ≃ Y) (hf : IsInducing ⇑f) : (f.toHomeomorphOfIsInducing hf).toEquiv = f

@[deprecated Equiv.toHomeomorphOfIsInducing]

def Equiv.toHomeomorphOfInducing {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X ≃ Y) (hf : IsInducing ⇑f) : X ≃ₜ Y

Alias of Equiv.toHomeomorphOfIsInducing.

---

An inducing equiv between topological spaces is a homeomorphism.

Equations

• @Equiv.toHomeomorphOfInducing = @Equiv.toHomeomorphOfIsInducing

theorem Continuous.continuous_symm_of_equiv_compact_to_t2 {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [CompactSpace X] [T2Space Y] {f : X ≃ Y} (hf : Continuous ⇑f) : Continuous ⇑f.symm

def Continuous.homeoOfEquivCompactToT2 {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [CompactSpace X] [T2Space Y] {f : X ≃ Y} (hf : Continuous ⇑f) : X ≃ₜ 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 := ⋯ }

@[simp]

theorem Continuous.homeoOfEquivCompactToT2_toEquiv {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [CompactSpace X] [T2Space Y] {f : X ≃ Y} (hf : Continuous ⇑f) : hf.homeoOfEquivCompactToT2.toEquiv = f

structure IsHomeomorph {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) : Prop

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

theorem IsHomeomorph.continuous {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (self : IsHomeomorph f) : Continuous f

theorem IsHomeomorph.isOpenMap {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (self : IsHomeomorph f) : IsOpenMap f

theorem IsHomeomorph.bijective {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (self : IsHomeomorph f) : Function.Bijective f

theorem Homeomorph.isHomeomorph {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) : IsHomeomorph ⇑h

theorem IsHomeomorph.injective {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : IsHomeomorph f) : Function.Injective f

theorem IsHomeomorph.surjective {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : IsHomeomorph f) : Function.Surjective f

noncomputable def IsHomeomorph.homeomorph {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) (hf : IsHomeomorph f) : X ≃ₜ Y

Bundled homeomorphism constructed from a map that is a homeomorphism.

Equations

• IsHomeomorph.homeomorph f hf = { toEquiv := Equiv.ofBijective f ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem IsHomeomorph.homeomorph_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) (hf : IsHomeomorph f) : ∀ (a : X), (IsHomeomorph.homeomorph f hf) a = f a

@[simp]

theorem IsHomeomorph.homeomorph_toEquiv {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) (hf : IsHomeomorph f) : (IsHomeomorph.homeomorph f hf).toEquiv = Equiv.ofBijective f ⋯

@[simp]

theorem IsHomeomorph.homeomorph_symm_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) (hf : IsHomeomorph f) (b : Y) : (IsHomeomorph.homeomorph f hf).symm b = Function.surjInv ⋯ b

theorem IsHomeomorph.isClosedMap {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : IsHomeomorph f) : IsClosedMap f

theorem IsHomeomorph.isInducing {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : IsHomeomorph f) : IsInducing f

theorem IsHomeomorph.isQuotientMap {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : IsHomeomorph f) : IsQuotientMap f

theorem IsHomeomorph.isEmbedding {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : IsHomeomorph f) : IsEmbedding f

theorem IsHomeomorph.isOpenEmbedding {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : IsHomeomorph f) : IsOpenEmbedding f

theorem IsHomeomorph.isClosedEmbedding {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : IsHomeomorph f) : IsClosedEmbedding f

theorem IsHomeomorph.isDenseEmbedding {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : IsHomeomorph f) : IsDenseEmbedding f

@[deprecated IsHomeomorph.isInducing]

theorem IsHomeomorph.inducing {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : IsHomeomorph f) : IsInducing f

Alias of IsHomeomorph.isInducing.

@[deprecated IsHomeomorph.isEmbedding]

theorem IsHomeomorph.embedding {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : IsHomeomorph f) : IsEmbedding f

Alias of IsHomeomorph.isEmbedding.

@[deprecated IsHomeomorph.isQuotientMap]

theorem IsHomeomorph.quotientMap {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : IsHomeomorph f) : IsQuotientMap f

Alias of IsHomeomorph.isQuotientMap.

@[deprecated IsHomeomorph.isClosedEmbedding]

theorem IsHomeomorph.closedEmbedding {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : IsHomeomorph f) : IsClosedEmbedding f

Alias of IsHomeomorph.isClosedEmbedding.

@[deprecated IsHomeomorph.isOpenEmbedding]

theorem IsHomeomorph.openEmbedding {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : IsHomeomorph f) : IsOpenEmbedding f

Alias of IsHomeomorph.isOpenEmbedding.

@[deprecated IsHomeomorph.isDenseEmbedding]

theorem IsHomeomorph.denseEmbedding {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : IsHomeomorph f) : IsDenseEmbedding f

Alias of IsHomeomorph.isDenseEmbedding.

theorem isHomeomorph_iff_exists_homeomorph {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} : IsHomeomorph f ↔ ∃ (h : X ≃ₜ Y), ⇑h = f

A map is a homeomorphism iff it is the map underlying a bundled homeomorphism h : X ≃ₜ Y.

theorem isHomeomorph_iff_exists_inverse {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} : IsHomeomorph f ↔ Continuous f ∧ ∃ (g : Y → X), Function.LeftInverse g f ∧ Function.RightInverse g f ∧ Continuous g

A map is a homeomorphism iff it is continuous and has a continuous inverse.

theorem isHomeomorph_iff_isEmbedding_surjective {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} : IsHomeomorph f ↔ IsEmbedding f ∧ Function.Surjective f

A map is a homeomorphism iff it is a surjective embedding.

@[deprecated isHomeomorph_iff_isEmbedding_surjective]

theorem isHomeomorph_iff_embedding_surjective {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} : IsHomeomorph f ↔ IsEmbedding f ∧ Function.Surjective f

Alias of isHomeomorph_iff_isEmbedding_surjective.

---

A map is a homeomorphism iff it is a surjective embedding.

theorem isHomeomorph_iff_continuous_isClosedMap_bijective {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} : IsHomeomorph f ↔ Continuous f ∧ IsClosedMap f ∧ Function.Bijective f

A map is a homeomorphism iff it is continuous, closed and bijective.

theorem isHomeomorph_iff_continuous_bijective {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} [CompactSpace X] [T2Space Y] : IsHomeomorph f ↔ Continuous f ∧ Function.Bijective f

A map from a compact space to a T2 space is a homeomorphism iff it is continuous and bijective.

theorem IsHomeomorph.id {X : Type u_1} [TopologicalSpace X] : IsHomeomorph id

theorem IsHomeomorph.comp {X : Type u_1} {Y : Type u_2} {Z : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : X → Y} {g : Y → Z} (hg : IsHomeomorph g) (hf : IsHomeomorph f) : IsHomeomorph (g ∘ f)

theorem IsHomeomorph.sumMap {X : Type u_1} {Y : Type u_2} {Z : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {W : Type u_5} [TopologicalSpace W] {f : X → Y} {g : Z → W} (hf : IsHomeomorph f) (hg : IsHomeomorph g) : IsHomeomorph (Sum.map f g)

theorem IsHomeomorph.prodMap {X : Type u_1} {Y : Type u_2} {Z : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {W : Type u_5} [TopologicalSpace W] {f : X → Y} {g : Z → W} (hf : IsHomeomorph f) (hg : IsHomeomorph g) : IsHomeomorph (Prod.map f g)

theorem IsHomeomorph.sigmaMap {ι : Type u_6} {κ : Type u_7} {X : ι → Type u_8} {Y : κ → Type u_9} [(i : ι) → TopologicalSpace (X i)] [(i : κ) → TopologicalSpace (Y i)] {f : ι → κ} (hf : Function.Bijective f) {g : (i : ι) → X i → Y (f i)} (hg : ∀ (i : ι), IsHomeomorph (g i)) : IsHomeomorph (Sigma.map f g)

theorem IsHomeomorph.pi_map {ι : Type u_6} {X : ι → Type u_7} {Y : ι → Type u_8} [(i : ι) → TopologicalSpace (X i)] [(i : ι) → TopologicalSpace (Y i)] {f : (i : ι) → X i → Y i} (h : ∀ (i : ι), IsHomeomorph (f i)) : IsHomeomorph fun (x : (i : ι) → X i) (i : ι) => f i (x i)