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_4) (Y : Type u_5) [TopologicalSpace X] [TopologicalSpace Y] extends Equiv : Type (max u_4 u_5)

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_4} {Y : Type u_5} [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_4} {Y : Type u_5} [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' := ⋯ }

instance Homeomorph.instCoeFunForall {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] : CoeFun (X ≃ₜ Y) fun (x : X ≃ₜ Y) => X → Y

Equations

• Homeomorph.instCoeFunForall = { coe := DFunLike.coe }

@[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 = let __spread.0 := Equiv.equivOfIsEmpty X Y; { toEquiv := __spread.0, 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'

@[simp]

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

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

Identity map as a homeomorphism.

Equations

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

def Homeomorph.trans {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [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_3} [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_3} [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.inducing {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) : Inducing ⇑h

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.quotientMap {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) : QuotientMap ⇑h

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.embedding {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) : Embedding ⇑h

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

Homeomorphism given an embedding.

Equations

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

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.t3Space {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T3Space X] (h : X ≃ₜ Y) : T3Space Y

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

@[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.openEmbedding {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) : OpenEmbedding ⇑h

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

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.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 HasCompactSupport.comp_homeomorph {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {M : Type u_6} [Zero M] {f : Y → M} (hf : HasCompactSupport f) (φ : X ≃ₜ Y) : HasCompactSupport (f ∘ ⇑φ)

theorem HasCompactMulSupport.comp_homeomorph {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {M : Type u_6} [One M] {f : Y → M} (hf : HasCompactMulSupport f) (φ : X ≃ₜ Y) : HasCompactMulSupport (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)

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.comp_continuousOn_iff {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [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_3} [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_3} [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_3} [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_3} [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_3} [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_3} [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_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (h : X ≃ₜ Y) {f : Y → Z} : IsOpenMap (f ∘ ⇑h) ↔ IsOpenMap f

@[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_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 // (fun (a : X) => p a) a }) : ↑((h.subtype h_iff) a) = h ↑a

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 = let __spread.0 := h.subtypeEquiv h_iff; { toEquiv := __spread.0, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[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_4} {Y' : Type u_5} [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_4} {Y' : Type u_5} [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_4} {Y' : Type u_5} [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_4} {Y' : Type u_5} [TopologicalSpace X'] [TopologicalSpace Y'] (h₁ : X ≃ₜ X') (h₂ : Y ≃ₜ Y') : ⇑(h₁.prodCongr h₂) = Prod.map ⇑h₁ ⇑h₂

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_3) [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.prodPUnit_apply (X : Type u_1) [TopologicalSpace X] : ⇑(Homeomorph.prodPUnit X) = fun (p : X × PUnit.{u_6 + 1} ) => p.1

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

X × {*} is homeomorphic to X.

Equations

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

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

{*} × X is homeomorphic to X.

Equations

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

@[simp]

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

@[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

@[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

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 = let __src := Equiv.equivOfUnique X Y; { toEquiv := __src, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem Homeomorph.piCongrLeft_apply {ι : Type u_6} {ι' : Type u_7} {Y : ι' → Type u_8} [(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_6} {ι' : Type u_7} {Y : ι' → Type u_8} [(j : ι') → TopologicalSpace (Y j)] (e : ι ≃ ι') : (Homeomorph.piCongrLeft e).toEquiv = Equiv.piCongrLeft Y e

def Homeomorph.piCongrLeft {ι : Type u_6} {ι' : Type u_7} {Y : ι' → Type u_8} [(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.piCongrRight_apply {ι : Type u_6} {Y₁ : ι → Type u_7} {Y₂ : ι → Type u_8} [(i : ι) → TopologicalSpace (Y₁ i)] [(i : ι) → TopologicalSpace (Y₂ i)] (F : (i : ι) → Y₁ i ≃ₜ Y₂ i) (H : (a : ι) → (fun (i : ι) => Y₁ i) a) (a : ι) : (Homeomorph.piCongrRight F) H a = (F a) (H a)

@[simp]

theorem Homeomorph.piCongrRight_toEquiv {ι : Type u_6} {Y₁ : ι → Type u_7} {Y₂ : ι → Type u_8} [(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

def Homeomorph.piCongrRight {ι : Type u_6} {Y₁ : ι → Type u_7} {Y₂ : ι → Type u_8} [(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_symm {ι : Type u_6} {Y₁ : ι → Type u_7} {Y₂ : ι → Type u_8} [(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

@[simp]

theorem Homeomorph.piCongr_apply {ι₁ : Type u_6} {ι₂ : Type u_7} {Y₁ : ι₁ → Type u_8} {Y₂ : ι₂ → Type u_9} [(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_6} {ι₂ : Type u_7} {Y₁ : ι₁ → Type u_8} {Y₂ : ι₂ → Type u_9} [(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.piCongr {ι₁ : Type u_6} {ι₂ : Type u_7} {Y₁ : ι₁ → Type u_8} {Y₂ : ι₂ → Type u_9} [(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)

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.sumProdDistrib {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [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

def Homeomorph.prodSumDistrib {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [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_6} {X : ι → Type u_7} [(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.funUnique_symm_apply (ι : Type u_6) (X : Type u_7) [Unique ι] [TopologicalSpace X] : ⇑(Homeomorph.funUnique ι X).symm = uniqueElim

@[simp]

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

def Homeomorph.funUnique (ι : Type u_6) (X : Type u_7) [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.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.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.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.finTwoArrow {X : Type u_1} [TopologicalSpace X] : (Fin 2 → X) ≃ₜ X × X

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

Equations

• Homeomorph.finTwoArrow = let __src := Homeomorph.piFinTwo fun (x : Fin 2) => X; { toEquiv := finTwoArrowEquiv X, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[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

@[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

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.Set.univ_symm_apply_coe (X : Type u_6) [TopologicalSpace X] (a : X) : ↑((Homeomorph.Set.univ X).symm a) = a

@[simp]

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

def Homeomorph.Set.univ (X : Type u_6) [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.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)

@[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, ⋯⟩)

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.piEquivPiSubtypeProd_symm_apply {ι : Type u_6} (p : ι → Prop) (Y : ι → Type u_7) [(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_6} (p : ι → Prop) (Y : ι → Type u_7) [(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.piEquivPiSubtypeProd {ι : Type u_6} (p : ι → Prop) (Y : ι → Type u_7) [(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.piSplitAt_symm_apply {ι : Type u_6} [DecidableEq ι] (i : ι) (Y : ι → Type u_7) [(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⟩

@[simp]

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

def Homeomorph.piSplitAt {ι : Type u_6} [DecidableEq ι] (i : ι) (Y : ι → Type u_7) [(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.funSplitAt_apply (Y : Type u_2) [TopologicalSpace Y] {ι : Type u_6} [DecidableEq ι] (i : ι) (f : (j : ι) → (fun (a : ι) => Y) j) : (Homeomorph.funSplitAt Y i) f = (f i, fun (j : { j : ι // ¬j = i }) => f ↑j)

@[simp]

theorem Homeomorph.funSplitAt_symm_apply (Y : Type u_2) [TopologicalSpace Y] {ι : Type u_6} [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, ⋯⟩

def Homeomorph.funSplitAt (Y : Type u_2) [TopologicalSpace Y] {ι : Type u_6} [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 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

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.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_4} [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)

@[simp]

theorem Equiv.toHomeomorphOfInducing_toEquiv {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X ≃ Y) (hf : Inducing ⇑f) : (f.toHomeomorphOfInducing hf).toEquiv = f

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

An inducing equiv between topological spaces is a homeomorphism.

Equations

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

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

@[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

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