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 α β: The type of homeomorphisms from α to β. This type can be denoted using the following notation: α ≃ₜ β.

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 (α : Type u_5) (β : Type u_6) [TopologicalSpace α] [TopologicalSpace β] extends Equiv : Type (max u_5 u_6)

• toFun : α → β
• invFun : β → α
• left_inv : Function.LeftInverse s.invFun s.toFun
• right_inv : Function.RightInverse s.invFun s.toFun
• continuous_toFun : Continuous s.toFun

  The forward map of a homeomorphism is a continuous function.

• continuous_invFun : Continuous s.invFun

  The inverse map of a homeomorphism is a continuous function.

Homeomorphism between α and β, also called topological isomorphism

def «term_≃ₜ_» : Lean.TrailingParserDescr

Homeomorphism between α and β, 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 {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] : Function.Injective Homeomorph.toEquiv

instance Homeomorph.instEquivLikeHomeomorph {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] : EquivLike (α ≃ₜ β) α β

Equations

• One or more equations did not get rendered due to their size.

instance Homeomorph.instCoeFunHomeomorphForAll {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] : CoeFun (α ≃ₜ β) fun x => α → β

Equations

• Homeomorph.instCoeFunHomeomorphForAll = { coe := FunLike.coe }

@[simp]

theorem Homeomorph.homeomorph_mk_coe {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (a : α ≃ β) (b : Continuous a.toFun) (c : Continuous a.invFun) : ↑(Homeomorph.mk a) = ↑a

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

Inverse of a homeomorphism.

Equations

• Homeomorph.symm h = Homeomorph.mk h.symm

@[simp]

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

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

See Note [custom simps projection]

Equations

• Homeomorph.Simps.symm_apply h = ↑(Homeomorph.symm h)

@[simp]

theorem Homeomorph.coe_toEquiv {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (h : α ≃ₜ β) : ↑h.toEquiv = ↑h

@[simp]

theorem Homeomorph.coe_symm_toEquiv {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (h : α ≃ₜ β) : ↑h.symm = ↑(Homeomorph.symm h)

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

@[simp]

theorem Homeomorph.refl_apply (α : Type u_5) [TopologicalSpace α] : ↑(Homeomorph.refl α) = id

def Homeomorph.refl (α : Type u_5) [TopologicalSpace α] : α ≃ₜ α

Identity map as a homeomorphism.

Equations

• Homeomorph.refl α = Homeomorph.mk (Equiv.refl α)

def Homeomorph.trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (h₁ : α ≃ₜ β) (h₂ : β ≃ₜ γ) : α ≃ₜ γ

Composition of two homeomorphisms.

Equations

• Homeomorph.trans h₁ h₂ = Homeomorph.mk (h₁.trans h₂.toEquiv)

@[simp]

theorem Homeomorph.trans_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (h₁ : α ≃ₜ β) (h₂ : β ≃ₜ γ) (a : α) : ↑(Homeomorph.trans h₁ h₂) a = ↑h₂ (↑h₁ a)

@[simp]

theorem Homeomorph.symm_trans_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (f : α ≃ₜ β) (g : β ≃ₜ γ) (a : γ) : ↑(Homeomorph.symm (Homeomorph.trans f g)) a = ↑(Homeomorph.symm f) (↑(Homeomorph.symm g) a)

@[simp]

theorem Homeomorph.homeomorph_mk_coe_symm {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (a : α ≃ β) (b : Continuous a.toFun) (c : Continuous a.invFun) : ↑(Homeomorph.symm (Homeomorph.mk a)) = ↑a.symm

@[simp]

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

theorem Homeomorph.continuous {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (h : α ≃ₜ β) : Continuous ↑h

theorem Homeomorph.continuous_symm {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (h : α ≃ₜ β) : Continuous ↑(Homeomorph.symm h)

@[simp]

theorem Homeomorph.apply_symm_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (h : α ≃ₜ β) (x : β) : ↑h (↑(Homeomorph.symm h) x) = x

@[simp]

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

@[simp]

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

@[simp]

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

theorem Homeomorph.bijective {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (h : α ≃ₜ β) : Function.Bijective ↑h

theorem Homeomorph.injective {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (h : α ≃ₜ β) : Function.Injective ↑h

theorem Homeomorph.surjective {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (h : α ≃ₜ β) : Function.Surjective ↑h

def Homeomorph.changeInv {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (f : α ≃ₜ β) (g : β → α) (hg : Function.RightInverse g ↑f) : α ≃ₜ β

Change the homeomorphism f to make the inverse function definitionally equal to g.

Equations

• Homeomorph.changeInv f g hg = Homeomorph.mk { toFun := ↑f, invFun := g, left_inv := (_ : Function.LeftInverse g ↑f), right_inv := (_ : Function.RightInverse g ↑f) }

@[simp]

theorem Homeomorph.symm_comp_self {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (h : α ≃ₜ β) : ↑(Homeomorph.symm h) ∘ ↑h = id

@[simp]

theorem Homeomorph.self_comp_symm {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (h : α ≃ₜ β) : ↑h ∘ ↑(Homeomorph.symm h) = id

@[simp]

theorem Homeomorph.range_coe {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (h : α ≃ₜ β) : Set.range ↑h = Set.univ

theorem Homeomorph.image_symm {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (h : α ≃ₜ β) : Set.image ↑(Homeomorph.symm h) = Set.preimage ↑h

theorem Homeomorph.preimage_symm {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (h : α ≃ₜ β) : Set.preimage ↑(Homeomorph.symm h) = Set.image ↑h

@[simp]

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

@[simp]

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

theorem Homeomorph.inducing {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (h : α ≃ₜ β) : Inducing ↑h

theorem Homeomorph.induced_eq {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (h : α ≃ₜ β) : TopologicalSpace.induced (↑h) inst✝ = inst✝¹

theorem Homeomorph.quotientMap {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (h : α ≃ₜ β) : QuotientMap ↑h

theorem Homeomorph.coinduced_eq {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (h : α ≃ₜ β) : TopologicalSpace.coinduced (↑h) inst✝ = inst✝¹

theorem Homeomorph.embedding {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (h : α ≃ₜ β) : Embedding ↑h

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

Homeomorphism given an embedding.

Equations

• Homeomorph.ofEmbedding f hf = Homeomorph.mk (Equiv.ofInjective f (_ : Function.Injective f))

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

theorem Homeomorph.isCompact_image {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s : Set α} (h : α ≃ₜ β) : IsCompact (↑h '' s) ↔ IsCompact s

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

@[simp]

theorem Homeomorph.isPreconnected_image {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s : Set α} (h : α ≃ₜ β) : IsPreconnected (↑h '' s) ↔ IsPreconnected s

@[simp]

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

@[simp]

theorem Homeomorph.isConnected_image {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s : Set α} (h : α ≃ₜ β) : IsConnected (↑h '' s) ↔ IsConnected s

@[simp]

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

@[simp]

theorem Homeomorph.comap_cocompact {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (h : α ≃ₜ β) : Filter.comap (↑h) (Filter.cocompact β) = Filter.cocompact α

@[simp]

theorem Homeomorph.map_cocompact {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (h : α ≃ₜ β) : Filter.map (↑h) (Filter.cocompact α) = Filter.cocompact β

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

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

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

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

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

theorem Homeomorph.denseEmbedding {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (h : α ≃ₜ β) : DenseEmbedding ↑h

@[simp]

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

@[simp]

theorem Homeomorph.isOpen_image {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (h : α ≃ₜ β) {s : Set α} : IsOpen (↑h '' s) ↔ IsOpen s

theorem Homeomorph.isOpenMap {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (h : α ≃ₜ β) : IsOpenMap ↑h

@[simp]

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

@[simp]

theorem Homeomorph.isClosed_image {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (h : α ≃ₜ β) {s : Set α} : IsClosed (↑h '' s) ↔ IsClosed s

theorem Homeomorph.isClosedMap {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (h : α ≃ₜ β) : IsClosedMap ↑h

theorem Homeomorph.openEmbedding {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (h : α ≃ₜ β) : OpenEmbedding ↑h

theorem Homeomorph.closedEmbedding {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (h : α ≃ₜ β) : ClosedEmbedding ↑h

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

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

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

theorem Homeomorph.image_closure {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (h : α ≃ₜ β) (s : Set α) : ↑h '' closure s = closure (↑h '' s)

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

theorem Homeomorph.image_interior {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (h : α ≃ₜ β) (s : Set α) : ↑h '' interior s = interior (↑h '' s)

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

theorem Homeomorph.image_frontier {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (h : α ≃ₜ β) (s : Set α) : ↑h '' frontier s = frontier (↑h '' s)

theorem HasCompactSupport.comp_homeomorph {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {M : Type u_5} [Zero M] {f : β → M} (hf : HasCompactSupport f) (φ : α ≃ₜ β) : HasCompactSupport (f ∘ ↑φ)

theorem HasCompactMulSupport.comp_homeomorph {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {M : Type u_5} [One M] {f : β → M} (hf : HasCompactMulSupport f) (φ : α ≃ₜ β) : HasCompactMulSupport (f ∘ ↑φ)

@[simp]

theorem Homeomorph.map_nhds_eq {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (h : α ≃ₜ β) (x : α) : Filter.map (↑h) (nhds x) = nhds (↑h x)

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

theorem Homeomorph.nhds_eq_comap {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (h : α ≃ₜ β) (x : α) : nhds x = Filter.comap (↑h) (nhds (↑h x))

@[simp]

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

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

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

def Homeomorph.homeomorphOfContinuousOpen {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : α ≃ β) (h₁ : Continuous ↑e) (h₂ : IsOpenMap ↑e) : α ≃ₜ β

If a bijective map e : α ≃ β is continuous and open, then it is a homeomorphism.

Equations

• Homeomorph.homeomorphOfContinuousOpen e h₁ h₂ = Homeomorph.mk e

@[simp]

theorem Homeomorph.comp_continuousOn_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (h : α ≃ₜ β) (f : γ → α) (s : Set γ) : ContinuousOn (↑h ∘ f) s ↔ ContinuousOn f s

@[simp]

theorem Homeomorph.comp_continuous_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (h : α ≃ₜ β) {f : γ → α} : Continuous (↑h ∘ f) ↔ Continuous f

@[simp]

theorem Homeomorph.comp_continuous_iff' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (h : α ≃ₜ β) {f : β → γ} : Continuous (f ∘ ↑h) ↔ Continuous f

theorem Homeomorph.comp_continuousAt_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (h : α ≃ₜ β) (f : γ → α) (x : γ) : ContinuousAt (↑h ∘ f) x ↔ ContinuousAt f x

theorem Homeomorph.comp_continuousAt_iff' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (h : α ≃ₜ β) (f : β → γ) (x : α) : ContinuousAt (f ∘ ↑h) x ↔ ContinuousAt f (↑h x)

theorem Homeomorph.comp_continuousWithinAt_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (h : α ≃ₜ β) (f : γ → α) (s : Set γ) (x : γ) : ContinuousWithinAt f s x ↔ ContinuousWithinAt (↑h ∘ f) s x

@[simp]

theorem Homeomorph.comp_isOpenMap_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (h : α ≃ₜ β) {f : γ → α} : IsOpenMap (↑h ∘ f) ↔ IsOpenMap f

@[simp]

theorem Homeomorph.comp_isOpenMap_iff' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (h : α ≃ₜ β) {f : β → γ} : IsOpenMap (f ∘ ↑h) ↔ IsOpenMap f

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

If two sets are equal, then they are homeomorphic.

Equations

• Homeomorph.setCongr h = Homeomorph.mk (Equiv.setCongr h)

def Homeomorph.sumCongr {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [TopologicalSpace δ] (h₁ : α ≃ₜ β) (h₂ : γ ≃ₜ δ) : α ⊕ γ ≃ₜ β ⊕ δ

Sum of two homeomorphisms.

Equations

• Homeomorph.sumCongr h₁ h₂ = Homeomorph.mk (Equiv.sumCongr h₁.toEquiv h₂.toEquiv)

def Homeomorph.prodCongr {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [TopologicalSpace δ] (h₁ : α ≃ₜ β) (h₂ : γ ≃ₜ δ) : α × γ ≃ₜ β × δ

Product of two homeomorphisms.

Equations

• Homeomorph.prodCongr h₁ h₂ = Homeomorph.mk (Equiv.prodCongr h₁.toEquiv h₂.toEquiv)

@[simp]

theorem Homeomorph.prodCongr_symm {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [TopologicalSpace δ] (h₁ : α ≃ₜ β) (h₂ : γ ≃ₜ δ) : Homeomorph.symm (Homeomorph.prodCongr h₁ h₂) = Homeomorph.prodCongr (Homeomorph.symm h₁) (Homeomorph.symm h₂)

@[simp]

theorem Homeomorph.coe_prodCongr {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [TopologicalSpace δ] (h₁ : α ≃ₜ β) (h₂ : γ ≃ₜ δ) : ↑(Homeomorph.prodCongr h₁ h₂) = Prod.map ↑h₁ ↑h₂

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

α × β is homeomorphic to β × α.

Equations

• Homeomorph.prodComm α β = Homeomorph.mk (Equiv.prodComm α β)

@[simp]

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

@[simp]

theorem Homeomorph.coe_prodComm (α : Type u_1) (β : Type u_2) [TopologicalSpace α] [TopologicalSpace β] : ↑(Homeomorph.prodComm α β) = Prod.swap

def Homeomorph.prodAssoc (α : Type u_1) (β : Type u_2) (γ : Type u_3) [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] : (α × β) × γ ≃ₜ α × β × γ

(α × β) × γ is homeomorphic to α × (β × γ).

Equations

• Homeomorph.prodAssoc α β γ = Homeomorph.mk (Equiv.prodAssoc α β γ)

@[simp]

theorem Homeomorph.prodPUnit_apply (α : Type u_1) [TopologicalSpace α] : ↑(Homeomorph.prodPUnit α) = fun p => p.fst

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

α × {*} is homeomorphic to α.

Equations

• Homeomorph.prodPUnit α = Homeomorph.mk (Equiv.prodPUnit α)

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

{*} × α is homeomorphic to α.

Equations

• Homeomorph.punitProd α = Homeomorph.trans (Homeomorph.prodComm PUnit.{u_5 + 1} α) (Homeomorph.prodPUnit α)

@[simp]

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

@[simp]

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

@[simp]

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

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

If both α and β have a unique element, then α ≃ₜ β.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

@[simp]

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

def Homeomorph.piCongrLeft {ι : Type u_5} {ι' : Type u_6} {β : ι' → Type u_7} [(j : ι') → TopologicalSpace (β j)] (e : ι ≃ ι') : ((i : ι) → β (↑e i)) ≃ₜ ((j : ι') → β j)

Equiv.piCongrLeft as a homeomorphism: this is the natural homeomorphism Π i, β (e i) ≃ₜ Π j, β j obtained from a bijection ι ≃ ι'.

Equations

• Homeomorph.piCongrLeft e = Homeomorph.mk (Equiv.piCongrLeft β e)

@[simp]

theorem Homeomorph.piCongrRight_apply {ι : Type u_5} {β₁ : ι → Type u_6} {β₂ : ι → Type u_7} [(i : ι) → TopologicalSpace (β₁ i)] [(i : ι) → TopologicalSpace (β₂ i)] (F : (i : ι) → β₁ i ≃ₜ β₂ i) (H : (a : ι) → (fun i => β₁ i) a) (a : ι) : ↑(Homeomorph.piCongrRight F) H a = ↑(F a) (H a)

@[simp]

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

def Homeomorph.piCongrRight {ι : Type u_5} {β₁ : ι → Type u_6} {β₂ : ι → Type u_7} [(i : ι) → TopologicalSpace (β₁ i)] [(i : ι) → TopologicalSpace (β₂ i)] (F : (i : ι) → β₁ i ≃ₜ β₂ i) : ((i : ι) → β₁ i) ≃ₜ ((i : ι) → β₂ i)

Equiv.piCongrRight as a homeomorphism: this is the natural homeomorphism Π i, β₁ i ≃ₜ Π j, β₂ i obtained from homeomorphisms β₁ i ≃ₜ β₂ i for each i.

Equations

• Homeomorph.piCongrRight F = Homeomorph.mk (Equiv.piCongrRight fun i => (F i).toEquiv)

@[simp]

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

@[simp]

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

@[simp]

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

def Homeomorph.piCongr {ι₁ : Type u_5} {ι₂ : Type u_6} {β₁ : ι₁ → Type u_7} {β₂ : ι₂ → Type u_8} [(i₁ : ι₁) → TopologicalSpace (β₁ i₁)] [(i₂ : ι₂) → TopologicalSpace (β₂ i₂)] (e : ι₁ ≃ ι₂) (F : (i₁ : ι₁) → β₁ i₁ ≃ₜ β₂ (↑e i₁)) : ((i₁ : ι₁) → β₁ i₁) ≃ₜ ((i₂ : ι₂) → β₂ i₂)

Equiv.piCongr as a homeomorphism: this is the natural homeomorphism Π i₁, β₁ i ≃ₜ Π i₂, β₂ i₂ obtained from a bijection ι₁ ≃ ι₂ and homeomorphisms β₁ i₁ ≃ₜ β₂ (e i₁) for each i₁ : ι₁.

Equations

• Homeomorph.piCongr e F = Homeomorph.trans (Homeomorph.piCongrRight F) (Homeomorph.piCongrLeft e)

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

ULift α is homeomorphic to α.

Equations

• Homeomorph.ulift = Homeomorph.mk Equiv.ulift

def Homeomorph.sumProdDistrib {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] : (α ⊕ β) × γ ≃ₜ α × γ ⊕ β × γ

(α ⊕ β) × γ is homeomorphic to α × γ ⊕ β × γ.

Equations

• One or more equations did not get rendered due to their size.

def Homeomorph.prodSumDistrib {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] : α × (β ⊕ γ) ≃ₜ α × β ⊕ α × γ

α × (β ⊕ γ) is homeomorphic to α × β ⊕ α × γ.

Equations

• One or more equations did not get rendered due to their size.

def Homeomorph.sigmaProdDistrib {β : Type u_2} [TopologicalSpace β] {ι : Type u_5} {σ : ι → Type u_6} [(i : ι) → TopologicalSpace (σ i)] : ((i : ι) × σ i) × β ≃ₜ (i : ι) × σ i × β

(Σ i, σ i) × β is homeomorphic to Σ i, (σ i × β).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Homeomorph.funUnique_symm_apply (ι : Type u_5) (α : Type u_6) [Unique ι] [TopologicalSpace α] : ↑(Homeomorph.symm (Homeomorph.funUnique ι α)) = fun x b => x

@[simp]

theorem Homeomorph.funUnique_apply (ι : Type u_5) (α : Type u_6) [Unique ι] [TopologicalSpace α] : ↑(Homeomorph.funUnique ι α) = fun f => f default

def Homeomorph.funUnique (ι : Type u_5) (α : Type u_6) [Unique ι] [TopologicalSpace α] : (ι → α) ≃ₜ α

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

Equations

• Homeomorph.funUnique ι α = Homeomorph.mk (Equiv.funUnique ι α)

@[simp]

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

@[simp]

theorem Homeomorph.piFinTwo_symm_apply (α : Fin 2 → Type u) [(i : Fin 2) → TopologicalSpace (α i)] : ↑(Homeomorph.symm (Homeomorph.piFinTwo α)) = fun p => Fin.cons p.fst (Fin.cons p.snd finZeroElim)

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

Homeomorphism between dependent functions Π i : Fin 2, α i and α 0 × α 1.

Equations

• Homeomorph.piFinTwo α = Homeomorph.mk (piFinTwoEquiv α)

@[simp]

theorem Homeomorph.finTwoArrow_symm_apply {α : Type u_1} [TopologicalSpace α] : ↑(Homeomorph.symm Homeomorph.finTwoArrow) = fun x => ![x.fst, x.snd]

@[simp]

theorem Homeomorph.finTwoArrow_apply {α : Type u_1} [TopologicalSpace α] : ↑Homeomorph.finTwoArrow = fun f => (f 0, f 1)

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

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

Equations

• Homeomorph.finTwoArrow = let src := Homeomorph.piFinTwo fun x => α; Homeomorph.mk (finTwoArrowEquiv α)

@[simp]

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

@[simp]

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

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

A subset of a topological space is homeomorphic to its image under a homeomorphism.

Equations

• Homeomorph.image e s = Homeomorph.mk (Equiv.image e.toEquiv s)

@[simp]

theorem Homeomorph.Set.univ_apply (α : Type u_5) [TopologicalSpace α] : ↑(Homeomorph.Set.univ α) = Subtype.val

@[simp]

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

def Homeomorph.Set.univ (α : Type u_5) [TopologicalSpace α] : ↑Set.univ ≃ₜ α

Set.univ α is homeomorphic to α.

Equations

• Homeomorph.Set.univ α = Homeomorph.mk (Equiv.Set.univ α)

@[simp]

theorem Homeomorph.Set.prod_symm_apply_coe {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (s : Set α) (t : Set β) (x : { a // s a } × { b // t b }) : ↑(↑(Homeomorph.symm (Homeomorph.Set.prod s t)) x) = (↑x.fst, ↑x.snd)

@[simp]

theorem Homeomorph.Set.prod_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (s : Set α) (t : Set β) (x : { c // s c.fst ∧ t c.snd }) : ↑(Homeomorph.Set.prod s t) x = ({ val := (↑x).fst, property := Equiv.subtypeProdEquivProd.proof_1 x }, { val := (↑x).snd, property := Equiv.subtypeProdEquivProd.proof_2 x })

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

s ×ˢ t is homeomorphic to s × t.

Equations

• Homeomorph.Set.prod s t = Homeomorph.mk (Equiv.Set.prod s t)

@[simp]

theorem Homeomorph.piEquivPiSubtypeProd_apply {ι : Type u_5} (p : ι → Prop) (β : ι → Type u_6) [(i : ι) → TopologicalSpace (β i)] [DecidablePred p] (f : (i : ι) → β i) : ↑(Homeomorph.piEquivPiSubtypeProd p β) f = (fun x => f ↑x, fun x => f ↑x)

@[simp]

theorem Homeomorph.piEquivPiSubtypeProd_symm_apply {ι : Type u_5} (p : ι → Prop) (β : ι → Type u_6) [(i : ι) → TopologicalSpace (β i)] [DecidablePred p] (f : ((i : { x // p x }) → β ↑i) × ((i : { x // ¬p x }) → β ↑i)) (x : ι) : ↑(Homeomorph.symm (Homeomorph.piEquivPiSubtypeProd p β)) f x = if h : p x then Prod.fst ((i : { x // p x }) → β ↑i) ((i : { x // ¬p x }) → β ↑i) f { val := x, property := h } else Prod.snd ((i : { x // p x }) → β ↑i) ((i : { x // ¬p x }) → β ↑i) f { val := x, property := h }

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

The topological space Π i, β 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 β = Homeomorph.mk (Equiv.piEquivPiSubtypeProd p β)

@[simp]

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

@[simp]

theorem Homeomorph.piSplitAt_symm_apply {ι : Type u_5} [DecidableEq ι] (i : ι) (β : ι → Type u_6) [(j : ι) → TopologicalSpace (β j)] (f : β i × ((j : { j // j ≠ i }) → β ↑j)) (j : ι) : ↑(Homeomorph.symm (Homeomorph.piSplitAt i β)) f j = if h : j = i then (_ : i = j) ▸ f.fst else Prod.snd (β i) ((j : { j // ¬j = i }) → β ↑j) f { val := j, property := h }

def Homeomorph.piSplitAt {ι : Type u_5} [DecidableEq ι] (i : ι) (β : ι → Type u_6) [(j : ι) → TopologicalSpace (β j)] : ((j : ι) → β j) ≃ₜ β i × ((j : { j // j ≠ i }) → β ↑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 β = Homeomorph.mk (Equiv.piSplitAt i β)

@[simp]

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

@[simp]

theorem Homeomorph.funSplitAt_symm_apply (β : Type u_2) [TopologicalSpace β] {ι : Type u_5} [DecidableEq ι] (i : ι) (f : (fun a => β) i × ((j : { j // j ≠ i }) → (fun a => β) ↑j)) (j : ι) : ↑(Homeomorph.symm (Homeomorph.funSplitAt β i)) f j = if h : j = i then f.fst else Prod.snd β ({ j // ¬j = i } → β) f { val := j, property := (_ : ¬j = i) }

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

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 β i = Homeomorph.piSplitAt i fun a => β

@[simp]

theorem Equiv.toHomeomorph_toEquiv {α : Type u_5} {β : Type u_6} [TopologicalSpace α] [TopologicalSpace β] (e : α ≃ β) (he : ∀ (s : Set β), IsOpen (↑e ⁻¹' s) ↔ IsOpen s) : (Equiv.toHomeomorph e he).toEquiv = e

def Equiv.toHomeomorph {α : Type u_5} {β : Type u_6} [TopologicalSpace α] [TopologicalSpace β] (e : α ≃ β) (he : ∀ (s : Set β), IsOpen (↑e ⁻¹' s) ↔ IsOpen s) : α ≃ₜ β

An equiv between topological spaces respecting openness is a homeomorphism.

Equations

• Equiv.toHomeomorph e he = Homeomorph.mk e

@[simp]

theorem Equiv.coe_toHomeomorph {α : Type u_5} {β : Type u_6} [TopologicalSpace α] [TopologicalSpace β] (e : α ≃ β) (he : ∀ (s : Set β), IsOpen (↑e ⁻¹' s) ↔ IsOpen s) : ↑(Equiv.toHomeomorph e he) = ↑e

theorem Equiv.toHomeomorph_apply {α : Type u_5} {β : Type u_6} [TopologicalSpace α] [TopologicalSpace β] (e : α ≃ β) (he : ∀ (s : Set β), IsOpen (↑e ⁻¹' s) ↔ IsOpen s) (a : α) : ↑(Equiv.toHomeomorph e he) a = ↑e a

@[simp]

theorem Equiv.toHomeomorph_refl {α : Type u_5} [TopologicalSpace α] : Equiv.toHomeomorph (Equiv.refl α) (_ : ∀ (_s : Set α), IsOpen (↑(Equiv.refl α) ⁻¹' _s) ↔ IsOpen (↑(Equiv.refl α) ⁻¹' _s)) = Homeomorph.refl α

@[simp]

theorem Equiv.toHomeomorph_symm {α : Type u_5} {β : Type u_6} [TopologicalSpace α] [TopologicalSpace β] (e : α ≃ β) (he : ∀ (s : Set β), IsOpen (↑e ⁻¹' s) ↔ IsOpen s) : Homeomorph.symm (Equiv.toHomeomorph e he) = Equiv.toHomeomorph e.symm (_ : ∀ (s : Set α), IsOpen (↑e.symm ⁻¹' s) ↔ IsOpen s)

theorem Equiv.toHomeomorph_trans {α : Type u_5} {β : Type u_6} {γ : Type u_7} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (e : α ≃ β) (f : β ≃ γ) (he : ∀ (s : Set β), IsOpen (↑e ⁻¹' s) ↔ IsOpen s) (hf : ∀ (s : Set γ), IsOpen (↑f ⁻¹' s) ↔ IsOpen s) : Equiv.toHomeomorph (e.trans f) (_ : ∀ (_s : Set γ), IsOpen (↑e ⁻¹' (↑f ⁻¹' _s)) ↔ IsOpen _s) = Homeomorph.trans (Equiv.toHomeomorph e he) (Equiv.toHomeomorph f hf)

@[simp]

theorem Equiv.toHomeomorphOfInducing_toEquiv {α : Type u_5} {β : Type u_6} [TopologicalSpace α] [TopologicalSpace β] (f : α ≃ β) (hf : Inducing ↑f) : (Equiv.toHomeomorphOfInducing f hf).toEquiv = f

def Equiv.toHomeomorphOfInducing {α : Type u_5} {β : Type u_6} [TopologicalSpace α] [TopologicalSpace β] (f : α ≃ β) (hf : Inducing ↑f) : α ≃ₜ β

An inducing equiv between topological spaces is a homeomorphism.

Equations

• One or more equations did not get rendered due to their size.

theorem Continuous.continuous_symm_of_equiv_compact_to_t2 {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [CompactSpace α] [T2Space β] {f : α ≃ β} (hf : Continuous ↑f) : Continuous ↑f.symm

@[simp]

theorem Continuous.homeoOfEquivCompactToT2_toEquiv {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [CompactSpace α] [T2Space β] {f : α ≃ β} (hf : Continuous ↑f) : (Continuous.homeoOfEquivCompactToT2 hf).toEquiv = f

def Continuous.homeoOfEquivCompactToT2 {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [CompactSpace α] [T2Space β] {f : α ≃ β} (hf : Continuous ↑f) : α ≃ₜ β

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

• One or more equations did not get rendered due to their size.