Further properties of homeomorphisms

This file proves further properties of homeomorphisms between topological spaces. Pretty much every topological property is preserved under homeomorphisms.

noncomputable def Topology.IsEmbedding.toHomeomorph {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.

@[simp]

theorem Topology.IsEmbedding.toHomeomorph_apply_coe {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : IsEmbedding f) (a : X) : ↑(hf.toHomeomorph a) = f a

@[deprecated Topology.IsEmbedding.toHomeomorph (since := "2025-04-16")]

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

Alias of Topology.IsEmbedding.toHomeomorph.

---

Homeomorphism given an embedding.

@[deprecated Topology.IsEmbedding.toHomeomorph (since := "2024-10-26")]

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

Alias of Topology.IsEmbedding.toHomeomorph.

---

Homeomorphism given an embedding.

noncomputable def Topology.IsEmbedding.toHomeomorphOfSurjective {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : IsEmbedding f) (hsurj : Function.Surjective f) : X ≃ₜ Y

A surjective embedding is a homeomorphism.

@[simp]

theorem Topology.IsEmbedding.toHomeomorphOfSurjective_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : IsEmbedding f) (hsurj : Function.Surjective f) (a✝ : X) : (hf.toHomeomorphOfSurjective hsurj) a✝ = f a✝

@[deprecated Topology.IsEmbedding.toHomeomorphOfSurjective (since := "2025-04-16")]

def Topology.IsEmbedding.toHomeomorph_of_surjective {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : IsEmbedding f) (hsurj : Function.Surjective f) : X ≃ₜ Y

Alias of Topology.IsEmbedding.toHomeomorphOfSurjective.

---

A surjective embedding is a homeomorphism.

@[deprecated Topology.IsEmbedding.toHomeomorphOfSurjective (since := "2024-10-26")]

def Embedding.toHomeomeomorph_of_surjective {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : Topology.IsEmbedding f) (hsurj : Function.Surjective f) : X ≃ₜ Y

Alias of Topology.IsEmbedding.toHomeomorphOfSurjective.

---

A surjective embedding is a homeomorphism.

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

theorem Homeomorph.totallyDisconnectedSpace {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) [tdc : TotallyDisconnectedSpace X] : TotallyDisconnectedSpace Y

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

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

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

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

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.

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

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

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

If two sets are equal, then they are homeomorphic.

def Homeomorph.sumPiEquivProdPi (S : Type u_7) (T : Type u_8) (A : S ⊕ T → Type u_9) [(st : S ⊕ T) → TopologicalSpace (A st)] : ((st : S ⊕ T) → A st) ≃ₜ ((s : S) → A (Sum.inl s)) × ((t : T) → A (Sum.inr t))

The product over S ⊕ T of a family of topological spaces is homeomorphic to the product of (the product over S) and (the product over T).

This is Equiv.sumPiEquivProdPi as a Homeomorph.

def Homeomorph.piUnique {α : Type u_7} [Unique α] (f : α → Type u_8) [(x : α) → TopologicalSpace (f x)] : ((t : α) → f t) ≃ₜ f default

The product Π t : α, f t of a family of topological spaces is homeomorphic to the space f ⬝ when α only contains ⬝.

This is Equiv.piUnique as a Homeomorph.

@[simp]

theorem Homeomorph.piUnique_apply {α : Type u_7} [Unique α] (f : α → Type u_8) [(x : α) → TopologicalSpace (f x)] : ⇑(piUnique f) = fun (f : (i : α) → f i) => f default

@[simp]

theorem Homeomorph.piUnique_symm_apply {α : Type u_7} [Unique α] (f : α → Type u_8) [(x : α) → TopologicalSpace (f x)] : ⇑(piUnique f).symm = uniqueElim

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 ι ≃ ι'.

@[simp]

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

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 : ι') : (piCongrLeft e) a✝ a = (Equiv.piCongrLeft' Y e.symm).symm a✝ a

@[simp]

theorem Homeomorph.piCongrLeft_refl {ι : Type u_7} {X : ι → Type u_8} [(i : ι) → TopologicalSpace (X i)] : piCongrLeft (Equiv.refl ι) = Homeomorph.refl ((i : ι) → X i)

@[simp]

theorem Homeomorph.piCongrLeft_symm_apply {ι : Type u_7} {ι' : Type u_8} {Y : ι' → Type u_9} [(j : ι') → TopologicalSpace (Y j)] (e : ι ≃ ι') : ⇑(piCongrLeft e).symm = fun (x1 : (j : ι') → Y j) (x2 : ι) => x1 (e x2)

@[simp]

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

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.

@[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) : (piCongrRight F).toEquiv = Equiv.piCongrRight fun (i : ι) => (F i).toEquiv

@[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 : ι) : (piCongrRight F) a✝ i = (F i) (a✝ i)

@[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) : (piCongrRight F).symm = 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₁ : ι₁.

@[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₂ : ι₂) : (piCongr e F) a✝ i₂ = (Equiv.piCongrLeft Y₂ e) ((Equiv.piCongrRight fun (i : ι₁) => (F i).toEquiv) a✝) 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₁)) : (piCongr e F).toEquiv = (Equiv.piCongrRight fun (i : ι₁) => (F i).toEquiv).trans (Equiv.piCongrLeft Y₂ e)

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

ULift X is homeomorphic to X.

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.

@[simp]

theorem Homeomorph.sumArrowHomeomorphProdArrow_apply {X : Type u_1} [TopologicalSpace X] {ι : Type u_7} {ι' : Type u_8} (f : ι ⊕ ι' → X) : 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✝ : ι ⊕ ι') : 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)) => 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

@[simp]

theorem Fin.appendHomeomorph_symm_apply {X : Type u_1} [TopologicalSpace X] (m n : ℕ) (f : Fin (m + n) → X) : (appendHomeomorph m n).symm f = (fun (i : Fin m) => f (castAdd n i), fun (i : Fin n) => f (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)) : (appendHomeomorph m n) fg a✝ = append fg.1 fg.2 a✝

@[simp]

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

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

@[simp]

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

@[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) : 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) : sigmaProdDistrib.symm a✝ = (⟨a✝.fst, a✝.snd.1⟩, a✝.snd.2)

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.

@[simp]

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

@[simp]

theorem Homeomorph.funUnique_symm_apply (ι : Type u_7) (X : Type u_8) [Unique ι] [TopologicalSpace X] : ⇑(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.

@[simp]

theorem Homeomorph.piFinTwo_apply (X : Fin 2 → Type u) [(i : Fin 2) → TopologicalSpace (X i)] : ⇑(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)] : ⇑(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.

@[simp]

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

@[simp]

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

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.

@[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.Set.univ (X : Type u_7) [TopologicalSpace X] : ↑_root_.Set.univ ≃ₜ X

Set.univ X is homeomorphic to X.

@[simp]

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

@[simp]

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

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.

@[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 }) : (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 }) : ↑((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.

@[simp]

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

@[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 : ι) : (piEquivPiSubtypeProd p Y).symm f x = if h : p x then f.1 ⟨x, h⟩ else f.2 ⟨x, h⟩

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.

@[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 : ι) : (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_7} [DecidableEq ι] (i : ι) (Y : ι → Type u_8) [(j : ι) → TopologicalSpace (Y j)] (f : (j : ι) → Y j) : (piSplitAt i Y) f = (f i, fun (j : { j : ι // ¬j = i }) => f ↑j)

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.

@[simp]

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

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

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

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.

@[simp]

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

@[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) : (homeomorph f hf) a✝ = f a✝

@[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) : (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) : Topology.IsInducing f

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

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

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

theorem IsHomeomorph.isClosedEmbedding {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : IsHomeomorph f) : Topology.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 (since := "2024-10-28")]

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

Alias of IsHomeomorph.isInducing.

@[deprecated IsHomeomorph.isEmbedding (since := "2024-10-26")]

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

Alias of IsHomeomorph.isEmbedding.

@[deprecated IsHomeomorph.isQuotientMap (since := "2024-10-22")]

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

Alias of IsHomeomorph.isQuotientMap.

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 ↔ Topology.IsEmbedding f ∧ Function.Surjective f

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

@[deprecated isHomeomorph_iff_isEmbedding_surjective (since := "2024-10-26")]

theorem isHomeomorph_iff_embedding_surjective {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} : IsHomeomorph f ↔ Topology.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.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)