Documentation

Mathlib.Topology.Homeomorph.Lemmas

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 Homeomorph.ofIsEmbedding {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : XY) (hf : Topology.IsEmbedding f) :
X ≃ₜ (Set.range f)

Homeomorphism given an embedding.

Equations
@[deprecated Homeomorph.ofIsEmbedding (since := "2024-10-26")]
def Homeomorph.ofEmbedding {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : XY) (hf : Topology.IsEmbedding f) :
X ≃ₜ (Set.range f)

Alias of Homeomorph.ofIsEmbedding.


Homeomorphism given an embedding.

Equations
@[simp]
theorem Homeomorph.isCompact_image {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {s : Set X} (h : X ≃ₜ Y) :

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

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

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

@[simp]

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) :
@[simp]
@[simp]
theorem Homeomorph.isConnected_image {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {s : Set X} (h : X ≃ₜ Y) :
@[simp]
theorem Homeomorph.isConnected_preimage {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {s : Set Y} (h : X ≃ₜ Y) :
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) :
theorem Homeomorph.t0Space {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T0Space X] (h : X ≃ₜ Y) :
theorem Homeomorph.t1Space {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T1Space X] (h : X ≃ₜ Y) :
theorem Homeomorph.t2Space {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T2Space X] (h : X ≃ₜ Y) :
theorem Homeomorph.t25Space {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T25Space X] (h : X ≃ₜ Y) :
theorem Homeomorph.t3Space {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T3Space X] (h : X ≃ₜ Y) :
theorem Homeomorph.t4Space {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T4Space X] (h : X ≃ₜ Y) :
theorem Homeomorph.t5Space {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T5Space X] (h : X ≃ₜ Y) :
@[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) :
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)

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

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

@[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 : ZX) (s : Set Z) :
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 : ZX) (s : Set Z) (z : Z) :
def Homeomorph.subtype {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {p : XProp} {q : YProp} (h : X ≃ₜ Y) (h_iff : ∀ (x : X), p x q (h x)) :
{ x : X // p x } ≃ₜ { y : Y // q y }

A homeomorphism h : X ≃ₜ Y lifts to a homeomorphism between subtypes corresponding to predicates p : X → Prop and q : Y → Prop so long as p = q ∘ h.

Equations
  • h.subtype h_iff = { toEquiv := h.subtypeEquiv h_iff, continuous_toFun := , continuous_invFun := }
@[simp]
theorem Homeomorph.subtype_apply_coe {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {p : XProp} {q : YProp} (h : X ≃ₜ Y) (h_iff : ∀ (x : X), p x q (h x)) (a : { a : X // p a }) :
((h.subtype h_iff) a) = h a
@[simp]
theorem Homeomorph.subtype_symm_apply_coe {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {p : XProp} {q : YProp} (h : X ≃ₜ Y) (h_iff : ∀ (x : X), p x q (h x)) (b : { b : Y // q b }) :
((h.subtype h_iff).symm b) = h.symm b
@[simp]
theorem Homeomorph.subtype_toEquiv {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {p : XProp} {q : YProp} (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
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.

Equations
def Homeomorph.sumPiEquivProdPi (S : Type u_7) (T : Type u_8) (A : S TType 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.

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

Equations
@[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)] :
def Homeomorph.piCongrLeft {ι : Type u_7} {ι' : Type u_8} {Y : ι'Type u_9} [(j : ι') → TopologicalSpace (Y j)] (e : ι ι') :
((i : ι) → Y (e i)) ≃ₜ ((j : ι') → Y j)

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

Equations
@[simp]
theorem Homeomorph.piCongrLeft_apply {ι : Type u_7} {ι' : Type u_8} {Y : ι'Type u_9} [(j : ι') → TopologicalSpace (Y j)] (e : ι ι') (a✝ : (b : ι) → Y (e.symm.symm b)) (a : ι') :
(piCongrLeft e) a✝ a = (Equiv.piCongrLeft' Y e.symm).symm a✝ a
@[simp]
theorem Homeomorph.piCongrLeft_toEquiv {ι : Type u_7} {ι' : Type u_8} {Y : ι'Type u_9} [(j : ι') → TopologicalSpace (Y j)] (e : ι ι') :
def Homeomorph.piCongrRight {ι : Type u_7} {Y₁ : ιType u_8} {Y₂ : ιType u_9} [(i : ι) → TopologicalSpace (Y₁ i)] [(i : ι) → TopologicalSpace (Y₂ i)] (F : (i : ι) → Y₁ i ≃ₜ Y₂ i) :
((i : ι) → Y₁ i) ≃ₜ ((i : ι) → Y₂ i)

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

Equations
@[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_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_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₁ : ι₁.

Equations
@[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₂ = (F (e.symm i₂)) (a✝ (e.symm i₂))
@[simp]
theorem Homeomorph.piCongr_toEquiv {ι₁ : Type u_7} {ι₂ : Type u_8} {Y₁ : ι₁Type u_9} {Y₂ : ι₂Type u_10} [(i₁ : ι₁) → TopologicalSpace (Y₁ i₁)] [(i₂ : ι₂) → TopologicalSpace (Y₂ i₂)] (e : ι₁ ι₂) (F : (i₁ : ι₁) → Y₁ i₁ ≃ₜ Y₂ (e i₁)) :
(piCongr e F).toEquiv = (Equiv.piCongrRight fun (i : ι₁) => (F i).toEquiv).trans (Equiv.piCongrLeft Y₂ e)

ULift X is homeomorphic to X.

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

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

Equations
@[simp]
theorem Homeomorph.sumArrowHomeomorphProdArrow_symm_apply {X : Type u_1} [TopologicalSpace X] {ι : Type u_7} {ι' : Type u_8} (p : (ιX) × (ι'X)) (a✝ : ι ι') :
@[simp]
theorem Fin.continuous_append {X : Type u_1} [TopologicalSpace X] (m n : ) :
Continuous fun (p : (Fin mX) × (Fin nX)) => append p.1 p.2
def Fin.appendHomeomorph {X : Type u_1} [TopologicalSpace X] (m n : ) :
(Fin mX) × (Fin nX) ≃ₜ (Fin (m + n)X)

The natural homeomorphism between (Fin m → X) × (Fin n → X) and Fin (m + n) → X. Fin.appendEquiv as a homeomorphism

Equations
@[simp]
theorem Fin.appendHomeomorph_apply {X : Type u_1} [TopologicalSpace X] (m n : ) (fg : (Fin mX) × (Fin nX)) (a✝ : Fin (m + n)) :
(appendHomeomorph m n) fg a✝ = append fg.1 fg.2 a✝
@[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))
def Homeomorph.sigmaProdDistrib {Y : Type u_2} [TopologicalSpace Y] {ι : Type u_7} {X : ιType u_8} [(i : ι) → TopologicalSpace (X i)] :
((i : ι) × X i) × Y ≃ₜ (i : ι) × X i × Y

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

Equations
@[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)
@[simp]
theorem Homeomorph.sigmaProdDistrib_toEquiv {Y : Type u_2} [TopologicalSpace Y] {ι : Type u_7} {X : ιType u_8} [(i : ι) → TopologicalSpace (X i)] :
def Homeomorph.funUnique (ι : Type u_7) (X : Type u_8) [Unique ι] [TopologicalSpace X] :
(ιX) ≃ₜ X

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

Equations
@[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] :
def Homeomorph.piFinTwo (X : Fin 2Type 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
@[simp]
theorem Homeomorph.piFinTwo_apply (X : Fin 2Type 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 2Type 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 2X) ≃ₜ X × X

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

Equations
@[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 2X) => (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.

Equations
  • e.image s = { toEquiv := e.image s, continuous_toFun := , continuous_invFun := }
@[simp]
theorem Homeomorph.image_apply_coe {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : X ≃ₜ Y) (s : Set X) (x : s) :
((e.image s) x) = e x
@[simp]
theorem Homeomorph.image_symm_apply_coe {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : X ≃ₜ Y) (s : Set X) (y : ↑(e.toEquiv '' s)) :
((e.image s).symm y) = e.symm y

Set.univ X is homeomorphic to X.

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

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

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

Equations
@[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)
@[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
def Homeomorph.funSplitAt (Y : Type u_2) [TopologicalSpace Y] {ι : Type u_7} [DecidableEq ι] (i : ι) :
(ιY) ≃ₜ Y × ({ j : ι // j i }Y)

A product of copies of a topological space can be split as the binary product of one copy and the product of all the remaining copies.

Equations
@[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,
@[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)
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
structure IsHomeomorph {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : XY) :

Predicate saying that f is a homeomorphism.

This should be used only when f is a concrete function whose continuous inverse is not easy to write down. Otherwise, Homeomorph should be preferred as it bundles the continuous inverse.

Having both Homeomorph and IsHomeomorph is justified by the fact that so many function properties are unbundled in the topology part of the library, and by the fact that a homeomorphism is not merely a continuous bijection, that is IsHomeomorph f is not equivalent to Continuous f ∧ Bijective f but to Continuous f ∧ Bijective f ∧ IsOpenMap f.

theorem Homeomorph.isHomeomorph {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) :
theorem IsHomeomorph.injective {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : XY} (hf : IsHomeomorph f) :
theorem IsHomeomorph.surjective {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : XY} (hf : IsHomeomorph f) :
noncomputable def IsHomeomorph.homeomorph {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : XY) (hf : IsHomeomorph f) :
X ≃ₜ Y

Bundled homeomorphism constructed from a map that is a homeomorphism.

Equations
@[simp]
theorem IsHomeomorph.homeomorph_toEquiv {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : XY) (hf : IsHomeomorph f) :
@[simp]
theorem IsHomeomorph.homeomorph_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : XY) (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 : XY) (hf : IsHomeomorph f) (b : Y) :
theorem IsHomeomorph.isClosedMap {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : XY} (hf : IsHomeomorph f) :
theorem IsHomeomorph.isInducing {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : XY} (hf : IsHomeomorph f) :
theorem IsHomeomorph.isEmbedding {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : XY} (hf : IsHomeomorph f) :
@[deprecated IsHomeomorph.isInducing (since := "2024-10-28")]
theorem IsHomeomorph.inducing {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : XY} (hf : IsHomeomorph 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 : XY} (hf : IsHomeomorph 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 : XY} (hf : IsHomeomorph f) :

Alias of IsHomeomorph.isQuotientMap.

@[deprecated IsHomeomorph.isClosedEmbedding (since := "2024-10-20")]

Alias of IsHomeomorph.isClosedEmbedding.

@[deprecated IsHomeomorph.isOpenEmbedding (since := "2024-10-18")]
theorem IsHomeomorph.openEmbedding {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : XY} (hf : IsHomeomorph f) :

Alias of IsHomeomorph.isOpenEmbedding.

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

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

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

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

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

Alias of isHomeomorph_iff_isEmbedding_surjective.


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

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

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

theorem IsHomeomorph.comp {X : Type u_1} {Y : Type u_2} {Z : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : XY} {g : YZ} (hg : IsHomeomorph g) (hf : IsHomeomorph f) :
theorem IsHomeomorph.sumMap {X : Type u_1} {Y : Type u_2} {Z : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {W : Type u_5} [TopologicalSpace W] {f : XY} {g : ZW} (hf : IsHomeomorph f) (hg : IsHomeomorph 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 : XY} {g : ZW} (hf : IsHomeomorph f) (hg : IsHomeomorph 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 iY (f i)} (hg : ∀ (i : ι), IsHomeomorph (g i)) :
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 iY i} (h : ∀ (i : ι), IsHomeomorph (f i)) :
IsHomeomorph fun (x : (i : ι) → X i) (i : ι) => f i (x i)