Mathlib.Topology.Homeomorph.Defs

Homeomorph structure

(X : Type*) (Y : Type*) [TopologicalSpace X] [TopologicalSpace Y]
    extends X ≃ Y

Full source

/-- Homeomorphism between `X` and `Y`, also called topological isomorphism -/
structure Homeomorph (X : Type*) (Y : Type*) [TopologicalSpace X] [TopologicalSpace Y]
    extends X ≃ Y where
  /-- The forward map of a homeomorphism is a continuous function. -/
  continuous_toFun : Continuous toFun := by continuity
  /-- The inverse map of a homeomorphism is a continuous function. -/
  continuous_invFun : Continuous invFun := by continuity

Homeomorphism between topological spaces

Informal description

A homeomorphism between topological spaces $X$ and $Y$ is a bijection $f : X \to Y$ such that both $f$ and its inverse $f^{-1}$ are continuous. This structure extends the notion of an equivalence between types by additionally requiring continuity in both directions.

term_≃ₜ_ definition

: Lean.TrailingParserDescr✝

Full source

@[inherit_doc]
infixl:25 " ≃ₜ " => Homeomorph

Homeomorphism notation

Informal description

The notation `X ≃ₜ Y` denotes the type of homeomorphisms between topological spaces `X` and `Y`, which are bijective continuous maps with continuous inverses.

Homeomorph.toEquiv_injective theorem

: Function.Injective (toEquiv : X ≃ₜ Y → X ≃ Y)

Full source

theorem toEquiv_injective : Function.Injective (toEquiv : X ≃ₜ Y → X ≃ Y)
  | ⟨_, _, _⟩, ⟨_, _, _⟩, rfl => rfl

Injectivity of the Homeomorphism-to-Equivalence Map

Informal description

The function that maps a homeomorphism between topological spaces $X$ and $Y$ to its underlying equivalence is injective. In other words, if two homeomorphisms $f, g : X \simeqₜ Y$ have the same underlying equivalence $f = g$ as bijections, then $f = g$ as homeomorphisms.

Homeomorph.instEquivLike instance

: EquivLike (X ≃ₜ Y) X Y

Full source

instance : EquivLike (X ≃ₜ Y) X Y where
  coe h := h.toEquiv
  inv h := h.toEquiv.symm
  left_inv h := h.left_inv
  right_inv h := h.right_inv
  coe_injective' _ _ H _ := toEquiv_injective <| DFunLike.ext' H

Homeomorphisms as Equivalence-like Objects

Informal description

The type of homeomorphisms $X \simeqₜ Y$ between topological spaces $X$ and $Y$ can be treated as a class of equivalence-like objects, where each homeomorphism can be injectively coerced to a bijection between $X$ and $Y$.

Homeomorph.homeomorph_mk_coe theorem

(a : X ≃ Y) (b c) : (Homeomorph.mk a b c : X → Y) = a

Full source

@[simp] theorem homeomorph_mk_coe (a : X ≃ Y) (b c) : (Homeomorph.mk a b c : X → Y) = a :=
  rfl

Homeomorphism Construction Preserves Underlying Function

Informal description

For any equivalence $a \colon X \simeq Y$ and any proofs $b$ and $c$ of continuity, the underlying function of the homeomorphism constructed from $a$, $b$, and $c$ is equal to $a$ as a function from $X$ to $Y$.

Homeomorph.empty definition

[IsEmpty X] [IsEmpty Y] : X ≃ₜ Y

Full source

/-- The unique homeomorphism between two empty types. -/
protected def empty [IsEmpty X] [IsEmpty Y] : X ≃ₜ Y where
  __ := Equiv.equivOfIsEmpty X Y

Homeomorphism between empty spaces

Informal description

The unique homeomorphism between two empty topological spaces $X$ and $Y$, constructed via the canonical equivalence between empty types.

Homeomorph.symm definition

(h : X ≃ₜ Y) : Y ≃ₜ X

Full source

/-- Inverse of a homeomorphism. -/
@[symm]
protected def symm (h : X ≃ₜ Y) : Y ≃ₜ X where
  continuous_toFun := h.continuous_invFun
  continuous_invFun := h.continuous_toFun
  toEquiv := h.toEquiv.symm

Inverse of a homeomorphism

Informal description

Given a homeomorphism $ h : X \simeq_{\text{top}} Y $ between topological spaces $ X $ and $ Y $, the inverse homeomorphism $ h^{-1} : Y \simeq_{\text{top}} X $ is defined by swapping the forward and inverse functions of $ h $, ensuring that $ h^{-1} $ is continuous in both directions.

Homeomorph.symm_symm theorem

(h : X ≃ₜ Y) : h.symm.symm = h

Full source

@[simp] theorem symm_symm (h : X ≃ₜ Y) : h.symm.symm = h := rfl

Double Inverse of a Homeomorphism is the Original Homeomorphism

Informal description

For any homeomorphism $h \colon X \simeq_{\text{top}} Y$ between topological spaces $X$ and $Y$, the double inverse of $h$ is equal to $h$ itself, i.e., $(h^{-1})^{-1} = h$.

Homeomorph.symm_bijective theorem

: Function.Bijective (Homeomorph.symm : (X ≃ₜ Y) → Y ≃ₜ X)

Full source

theorem symm_bijective : Function.Bijective (Homeomorph.symm : (X ≃ₜ Y) → Y ≃ₜ X) :=
  Function.bijective_iff_has_inverse.mpr ⟨_, symm_symm, symm_symm⟩

Bijectivity of the Homeomorphism Inverse Operation

Informal description

The inverse operation `Homeomorph.symm` that maps a homeomorphism $h \colon X \simeq_{\text{top}} Y$ to its inverse $h^{-1} \colon Y \simeq_{\text{top}} X$ is a bijective function from the set of homeomorphisms between $X$ and $Y$ to the set of homeomorphisms between $Y$ and $X$.

Homeomorph.Simps.symm_apply definition

(h : X ≃ₜ Y) : Y → X

Full source

/-- See Note [custom simps projection] -/
def Simps.symm_apply (h : X ≃ₜ Y) : Y → X :=
  h.symm

Inverse function of a homeomorphism

Informal description

For a homeomorphism $ h : X \simeq_{\text{top}} Y $ between topological spaces $ X $ and $ Y $, the function $ h^{-1} : Y \to X $ is the inverse of $ h $, mapping each element of $ Y $ back to its corresponding element in $ X $.

Homeomorph.coe_toEquiv theorem

(h : X ≃ₜ Y) : ⇑h.toEquiv = h

Full source

@[simp]
theorem coe_toEquiv (h : X ≃ₜ Y) : ⇑h.toEquiv = h :=
  rfl

Underlying Function of Homeomorphism Equivalence

Informal description

For any homeomorphism $h \colon X \simeq_{\text{top}} Y$ between topological spaces $X$ and $Y$, the underlying function of the equivalence $h.\text{toEquiv}$ is equal to $h$ itself.

Homeomorph.coe_symm_toEquiv theorem

(h : X ≃ₜ Y) : ⇑h.toEquiv.symm = h.symm

Full source

@[simp]
theorem coe_symm_toEquiv (h : X ≃ₜ Y) : ⇑h.toEquiv.symm = h.symm :=
  rfl

Inverse Homeomorphism Equals Inverse of Underlying Equivalence

Informal description

For any homeomorphism $h : X \simeq_{\text{top}} Y$ between topological spaces $X$ and $Y$, the underlying function of the inverse equivalence $h^{-1}$ (obtained via `h.toEquiv.symm`) coincides with the inverse homeomorphism $h^{-1}$ itself.

Homeomorph.ext theorem

{h h' : X ≃ₜ Y} (H : ∀ x, h x = h' x) : h = h'

Full source

@[ext]
theorem ext {h h' : X ≃ₜ Y} (H : ∀ x, h x = h' x) : h = h' :=
  DFunLike.ext _ _ H

Extensionality of Homeomorphisms

Informal description

For any two homeomorphisms $h, h' : X \simeqₜ Y$ between topological spaces $X$ and $Y$, if $h(x) = h'(x)$ for all $x \in X$, then $h = h'$.

Homeomorph.refl definition

(X : Type*) [TopologicalSpace X] : X ≃ₜ X

Full source

/-- Identity map as a homeomorphism. -/
@[simps! -fullyApplied apply]
protected def refl (X : Type*) [TopologicalSpace X] : X ≃ₜ X where
  continuous_toFun := continuous_id
  continuous_invFun := continuous_id
  toEquiv := Equiv.refl X

Identity homeomorphism

Informal description

The identity homeomorphism on a topological space $X$ is the bijection from $X$ to itself given by the identity function, with both the function and its inverse being continuous.

Homeomorph.trans definition

(h₁ : X ≃ₜ Y) (h₂ : Y ≃ₜ Z) : X ≃ₜ Z

Full source

/-- Composition of two homeomorphisms. -/
@[trans]
protected def trans (h₁ : X ≃ₜ Y) (h₂ : Y ≃ₜ Z) : X ≃ₜ Z where
  continuous_toFun := h₂.continuous_toFun.comp h₁.continuous_toFun
  continuous_invFun := h₁.continuous_invFun.comp h₂.continuous_invFun
  toEquiv := Equiv.trans h₁.toEquiv h₂.toEquiv

Composition of homeomorphisms

Informal description

Given two homeomorphisms $h₁ : X \simeq Y$ and $h₂ : Y \simeq Z$ between topological spaces, their composition $h₂ \circ h₁$ forms a homeomorphism $X \simeq Z$. The continuity of the composition follows from the continuity of both $h₁$ and $h₂$, and the continuity of the inverse follows from the continuity of their respective inverses.

Homeomorph.trans_apply theorem

(h₁ : X ≃ₜ Y) (h₂ : Y ≃ₜ Z) (x : X) : h₁.trans h₂ x = h₂ (h₁ x)

Full source

@[simp]
theorem trans_apply (h₁ : X ≃ₜ Y) (h₂ : Y ≃ₜ Z) (x : X) : h₁.trans h₂ x = h₂ (h₁ x) :=
  rfl

Composition of Homeomorphisms Evaluated at a Point: $(h₁ \circ h₂)(x) = h₂(h₁(x))$

Informal description

For any homeomorphisms $h₁ \colon X \simeq Y$ and $h₂ \colon Y \simeq Z$ between topological spaces and any point $x \in X$, the composition $h₁ \circ h₂$ evaluated at $x$ equals $h₂(h₁(x))$.

Homeomorph.symm_trans_apply theorem

(f : X ≃ₜ Y) (g : Y ≃ₜ Z) (z : Z) : (f.trans g).symm z = f.symm (g.symm z)

Full source

@[simp]
theorem symm_trans_apply (f : X ≃ₜ Y) (g : Y ≃ₜ Z) (z : Z) :
    (f.trans g).symm z = f.symm (g.symm z) := rfl

Inverse of Composition of Homeomorphisms Equals Composition of Inverses

Informal description

For any homeomorphisms $f \colon X \simeq Y$ and $g \colon Y \simeq Z$ between topological spaces, and for any point $z \in Z$, the inverse of the composition $f \circ g$ evaluated at $z$ equals the composition of the inverses $f^{-1} \circ g^{-1}$ evaluated at $z$, i.e., $(f \circ g)^{-1}(z) = f^{-1}(g^{-1}(z))$.

Homeomorph.homeomorph_mk_coe_symm theorem

(a : X ≃ Y) (b c) : ((Homeomorph.mk a b c).symm : Y → X) = a.symm

Full source

@[simp]
theorem homeomorph_mk_coe_symm (a : X ≃ Y) (b c) :
    ((Homeomorph.mk a b c).symm : Y → X) = a.symm :=
  rfl

Inverse Function of Constructed Homeomorphism Equals Bijection Inverse

Informal description

Let $X$ and $Y$ be topological spaces, and let $a : X \simeq Y$ be a bijection between them. For any proofs $b$ that $a$ is continuous and $c$ that $a^{-1}$ is continuous, the underlying function of the inverse homeomorphism $\text{Homeomorph.mk}(a, b, c)^{-1} \colon Y \to X$ equals the inverse bijection $a^{-1} \colon Y \to X$.

Homeomorph.refl_symm theorem

: (Homeomorph.refl X).symm = Homeomorph.refl X

Full source

@[simp]
theorem refl_symm : (Homeomorph.refl X).symm = Homeomorph.refl X :=
  rfl

Inverse of Identity Homeomorphism is Identity

Informal description

The inverse of the identity homeomorphism on a topological space $X$ is equal to the identity homeomorphism itself, i.e., $(\text{id}_X)^{-1} = \text{id}_X$.

Homeomorph.continuous theorem

(h : X ≃ₜ Y) : Continuous h

Full source

@[continuity, fun_prop]
protected theorem continuous (h : X ≃ₜ Y) : Continuous h :=
  h.continuous_toFun

Continuity of a Homeomorphism

Informal description

For any homeomorphism $h \colon X \simeqₜ Y$ between topological spaces $X$ and $Y$, the function $h$ is continuous.

Homeomorph.continuous_symm theorem

(h : X ≃ₜ Y) : Continuous h.symm

Full source

@[continuity]
protected theorem continuous_symm (h : X ≃ₜ Y) : Continuous h.symm :=
  h.continuous_invFun

Continuity of the Inverse of a Homeomorphism

Informal description

For any homeomorphism $h \colon X \simeq_{\text{top}} Y$ between topological spaces $X$ and $Y$, the inverse function $h^{-1} \colon Y \to X$ is continuous.

Homeomorph.apply_symm_apply theorem

(h : X ≃ₜ Y) (y : Y) : h (h.symm y) = y

Full source

@[simp]
theorem apply_symm_apply (h : X ≃ₜ Y) (y : Y) : h (h.symm y) = y :=
  h.toEquiv.apply_symm_apply y

Homeomorphism Recovery: $h(h^{-1}(y)) = y$

Informal description

For any homeomorphism $h \colon X \simeq_{\text{top}} Y$ between topological spaces $X$ and $Y$, and any point $y \in Y$, applying $h$ to the inverse image $h^{-1}(y)$ recovers the original point $y$, i.e., $h(h^{-1}(y)) = y$.

Homeomorph.symm_apply_apply theorem

(h : X ≃ₜ Y) (x : X) : h.symm (h x) = x

Full source

@[simp]
theorem symm_apply_apply (h : X ≃ₜ Y) (x : X) : h.symm (h x) = x :=
  h.toEquiv.symm_apply_apply x

Inverse Homeomorphism Recovers Original Point

Informal description

For any homeomorphism $h \colon X \simeq_{\text{top}} Y$ between topological spaces $X$ and $Y$, and any point $x \in X$, the inverse homeomorphism $h^{-1}$ applied to $h(x)$ recovers the original point $x$, i.e., $h^{-1}(h(x)) = x$.

Homeomorph.self_trans_symm theorem

(h : X ≃ₜ Y) : h.trans h.symm = Homeomorph.refl X

Full source

@[simp]
theorem self_trans_symm (h : X ≃ₜ Y) : h.trans h.symm = Homeomorph.refl X := by
  ext
  apply symm_apply_apply

Composition of Homeomorphism with its Inverse Yields Identity on Domain

Informal description

For any homeomorphism $h \colon X \simeq_{\text{top}} Y$ between topological spaces $X$ and $Y$, the composition of $h$ with its inverse $h^{-1}$ is equal to the identity homeomorphism on $X$, i.e., $h \circ h^{-1} = \text{id}_X$.

Homeomorph.symm_trans_self theorem

(h : X ≃ₜ Y) : h.symm.trans h = Homeomorph.refl Y

Full source

@[simp]
theorem symm_trans_self (h : X ≃ₜ Y) : h.symm.trans h = Homeomorph.refl Y := by
  ext
  apply apply_symm_apply

Inverse Composition Yields Identity on Codomain

Informal description

For any homeomorphism $h \colon X \simeq_{\text{top}} Y$ between topological spaces $X$ and $Y$, the composition of the inverse homeomorphism $h^{-1}$ with $h$ is equal to the identity homeomorphism on $Y$, i.e., $h^{-1} \circ h = \text{id}_Y$.

Homeomorph.bijective theorem

(h : X ≃ₜ Y) : Function.Bijective h

Full source

protected theorem bijective (h : X ≃ₜ Y) : Function.Bijective h :=
  h.toEquiv.bijective

Bijectivity of Homeomorphisms

Informal description

For any homeomorphism $h \colon X \simeq_{\text{top}} Y$ between topological spaces $X$ and $Y$, the function $h \colon X \to Y$ is bijective.

Homeomorph.injective theorem

(h : X ≃ₜ Y) : Function.Injective h

Full source

protected theorem injective (h : X ≃ₜ Y) : Function.Injective h :=
  h.toEquiv.injective

Injectivity of Homeomorphisms

Informal description

For any homeomorphism $h : X \simeqₜ Y$ between topological spaces $X$ and $Y$, the function $h : X \to Y$ is injective.

Homeomorph.surjective theorem

(h : X ≃ₜ Y) : Function.Surjective h

Full source

protected theorem surjective (h : X ≃ₜ Y) : Function.Surjective h :=
  h.toEquiv.surjective

Surjectivity of Homeomorphisms

Informal description

For any homeomorphism $h : X \simeqₜ Y$ between topological spaces $X$ and $Y$, the function $h : X \to Y$ is surjective.

Homeomorph.changeInv definition

(f : X ≃ₜ Y) (g : Y → X) (hg : Function.RightInverse g f) : X ≃ₜ Y

Full source

/-- Change the homeomorphism `f` to make the inverse function definitionally equal to `g`. -/
def changeInv (f : X ≃ₜ Y) (g : Y → X) (hg : Function.RightInverse g f) : X ≃ₜ Y :=
  haveI : g = f.symm := (f.left_inv.eq_rightInverse hg).symm
  { toFun := f
    invFun := g
    left_inv := by convert f.left_inv
    right_inv := by convert f.right_inv using 1
    continuous_toFun := f.continuous
    continuous_invFun := by convert f.symm.continuous }

Homeomorphism with specified inverse

Informal description

Given a homeomorphism $f \colon X \simeqₜ Y$ between topological spaces $X$ and $Y$, and a function $g \colon Y \to X$ that is a right inverse of $f$ (i.e., $f \circ g = \text{id}_Y$), the function `Homeomorph.changeInv` constructs a new homeomorphism from $X$ to $Y$ where the inverse function is definitionally equal to $g$.

Homeomorph.symm_comp_self theorem

(h : X ≃ₜ Y) : h.symm ∘ h = id

Full source

@[simp]
theorem symm_comp_self (h : X ≃ₜ Y) : h.symm ∘ h = id :=
  funext h.symm_apply_apply

Inverse Composition with Homeomorphism Yields Identity

Informal description

For any homeomorphism $h \colon X \simeq_{\text{top}} Y$ between topological spaces $X$ and $Y$, the composition of the inverse homeomorphism $h^{-1}$ with $h$ is equal to the identity function on $X$, i.e., $h^{-1} \circ h = \text{id}_X$.

Homeomorph.self_comp_symm theorem

(h : X ≃ₜ Y) : h ∘ h.symm = id

Full source

@[simp]
theorem self_comp_symm (h : X ≃ₜ Y) : h ∘ h.symm = id :=
  funext h.apply_symm_apply

Composition of Homeomorphism with its Inverse Yields Identity

Informal description

For any homeomorphism $h \colon X \simeq_{\text{top}} Y$ between topological spaces $X$ and $Y$, the composition of $h$ with its inverse $h^{-1}$ is equal to the identity function on $Y$, i.e., $h \circ h^{-1} = \text{id}_Y$.

Homeomorph.range_coe theorem

(h : X ≃ₜ Y) : range h = univ

Full source

theorem range_coe (h : X ≃ₜ Y) : range h = univ := by simp

Range of a Homeomorphism is the Universal Set

Informal description

For any homeomorphism $h : X \simeqₜ Y$ between topological spaces $X$ and $Y$, the range of $h$ is equal to the universal set of $Y$, i.e., $\text{range}(h) = \text{univ}$.

Homeomorph.image_symm theorem

(h : X ≃ₜ Y) : image h.symm = preimage h

Full source

theorem image_symm (h : X ≃ₜ Y) : image h.symm = preimage h :=
  funext h.symm.toEquiv.image_eq_preimage

Image under Inverse Homeomorphism Equals Preimage under Original Homeomorphism

Informal description

For any homeomorphism $h \colon X \simeq_{\text{top}} Y$ between topological spaces $X$ and $Y$, the image of a set under the inverse homeomorphism $h^{-1}$ equals the preimage under $h$, i.e., \[ h^{-1}(S) = h^{-1}(S) \] for any subset $S \subseteq Y$.

Homeomorph.preimage_symm theorem

(h : X ≃ₜ Y) : preimage h.symm = image h

Full source

theorem preimage_symm (h : X ≃ₜ Y) : preimage h.symm = image h :=
  (funext h.toEquiv.image_eq_preimage).symm

Preimage under Inverse Homeomorphism Equals Image under Original Homeomorphism

Informal description

For any homeomorphism $h \colon X \simeq_{\text{top}} Y$ between topological spaces $X$ and $Y$, the preimage under the inverse homeomorphism $h^{-1}$ is equal to the image under $h$, i.e., \[ h^{-1}^{-1}(S) = h(S) \] for any subset $S \subseteq X$.

Homeomorph.image_preimage theorem

(h : X ≃ₜ Y) (s : Set Y) : h '' (h ⁻¹' s) = s

Full source

@[simp]
theorem image_preimage (h : X ≃ₜ Y) (s : Set Y) : h '' (h ⁻¹' s) = s :=
  h.toEquiv.image_preimage s

Homeomorphism Preserves Image-Preimage Identity

Informal description

For any homeomorphism $h \colon X \to Y$ between topological spaces $X$ and $Y$, and any subset $s \subseteq Y$, the image of the preimage of $s$ under $h$ equals $s$ itself. In symbols, $h(h^{-1}(s)) = s$.

Homeomorph.preimage_image theorem

(h : X ≃ₜ Y) (s : Set X) : h ⁻¹' (h '' s) = s

Full source

@[simp]
theorem preimage_image (h : X ≃ₜ Y) (s : Set X) : h ⁻¹' (h '' s) = s :=
  h.toEquiv.preimage_image s

Preimage of Image under Homeomorphism is Identity

Informal description

For any homeomorphism $h : X \simeq Y$ between topological spaces $X$ and $Y$, and any subset $s \subseteq X$, the preimage of the image of $s$ under $h$ equals $s$ itself, i.e., $h^{-1}(h(s)) = s$.

Homeomorph.image_eq_preimage theorem

(h : X ≃ₜ Y) (s : Set X) : h '' s = h.symm ⁻¹' s

Full source

theorem image_eq_preimage (h : X ≃ₜ Y) (s : Set X) : h '' s = h.symm ⁻¹' s :=
  h.toEquiv.image_eq_preimage s

Image of a Set under a Homeomorphism Equals Preimage under its Inverse

Informal description

For any homeomorphism $h \colon X \simeq_{\text{top}} Y$ between topological spaces $X$ and $Y$, and any subset $s \subseteq X$, the image of $s$ under $h$ is equal to the preimage of $s$ under the inverse homeomorphism $h^{-1}$, i.e., \[ h(s) = h^{-1}^{-1}(s). \]

Homeomorph.image_compl theorem

(h : X ≃ₜ Y) (s : Set X) : h '' (sᶜ) = (h '' s)ᶜ

Full source

lemma image_compl (h : X ≃ₜ Y) (s : Set X) : h '' (sᶜ) = (h '' s)ᶜ :=
  h.toEquiv.image_compl s

Homeomorphism Preserves Complement of Image

Informal description

For any homeomorphism $h \colon X \to Y$ between topological spaces $X$ and $Y$, and any subset $s \subseteq X$, the image of the complement of $s$ under $h$ equals the complement of the image of $s$ under $h$. In symbols, $h(s^c) = (h(s))^c$.

Homeomorph.isInducing theorem

(h : X ≃ₜ Y) : IsInducing h

Full source

lemma isInducing (h : X ≃ₜ Y) : IsInducing h :=
  .of_comp h.continuous h.symm.continuous <| by simp only [symm_comp_self, IsInducing.id]

Homeomorphisms are Inducing Maps

Informal description

For any homeomorphism $h \colon X \simeq_{\text{top}} Y$ between topological spaces $X$ and $Y$, the function $h$ is inducing. That is, the topology on $X$ is the same as the topology induced by $h$ from $Y$.

Homeomorph.induced_eq theorem

(h : X ≃ₜ Y) : TopologicalSpace.induced h ‹_› = ‹_›

Full source

theorem induced_eq (h : X ≃ₜ Y) : TopologicalSpace.induced h ‹_› = ‹_› := h.isInducing.1.symm

Homeomorphism Preserves Induced Topology

Informal description

For any homeomorphism $h \colon X \simeq_{\text{top}} Y$ between topological spaces $X$ and $Y$, the topology on $X$ induced by $h$ is equal to the original topology on $X$.

Homeomorph.isQuotientMap theorem

(h : X ≃ₜ Y) : IsQuotientMap h

Full source

theorem isQuotientMap (h : X ≃ₜ Y) : IsQuotientMap h :=
  IsQuotientMap.of_comp h.symm.continuous h.continuous <| by
    simp only [self_comp_symm, IsQuotientMap.id]

Homeomorphisms are quotient maps

Informal description

For any homeomorphism $h \colon X \simeq_{\text{top}} Y$ between topological spaces $X$ and $Y$, the function $h$ is a quotient map. That is, $h$ is surjective and a subset $U \subseteq Y$ is open if and only if its preimage $h^{-1}(U)$ is open in $X$.

Homeomorph.coinduced_eq theorem

(h : X ≃ₜ Y) : TopologicalSpace.coinduced h ‹_› = ‹_›

Full source

theorem coinduced_eq (h : X ≃ₜ Y) : TopologicalSpace.coinduced h ‹_› = ‹_› :=
  h.isQuotientMap.2.symm

Coinduced Topology via Homeomorphism Equals Original Topology

Informal description

For any homeomorphism $h \colon X \simeq_{\text{top}} Y$ between topological spaces $X$ and $Y$, the coinduced topology on $Y$ via $h$ is equal to the original topology on $Y$. That is, the topology obtained by declaring a subset $U \subseteq Y$ to be open if and only if its preimage $h^{-1}(U)$ is open in $X$ coincides with the given topology on $Y$.

Homeomorph.isEmbedding theorem

(h : X ≃ₜ Y) : IsEmbedding h

Full source

theorem isEmbedding (h : X ≃ₜ Y) : IsEmbedding h := ⟨h.isInducing, h.injective⟩

Homeomorphisms are Topological Embeddings

Informal description

For any homeomorphism $h \colon X \simeq_{\text{top}} Y$ between topological spaces $X$ and $Y$, the function $h$ is a topological embedding. That is, $h$ is injective and the topology on $X$ is the coarsest topology that makes $h$ continuous.

Homeomorph.isOpen_preimage theorem

(h : X ≃ₜ Y) {s : Set Y} : IsOpen (h ⁻¹' s) ↔ IsOpen s

Full source

@[simp]
theorem isOpen_preimage (h : X ≃ₜ Y) {s : Set Y} : IsOpenIsOpen (h ⁻¹' s) ↔ IsOpen s :=
  h.isQuotientMap.isOpen_preimage

Openness Criterion for Preimages under Homeomorphisms

Informal description

For a homeomorphism $h \colon X \simeq_{\text{top}} Y$ between topological spaces $X$ and $Y$, and any subset $s \subseteq Y$, the preimage $h^{-1}(s)$ is open in $X$ if and only if $s$ is open in $Y$.

Homeomorph.isOpen_image theorem

(h : X ≃ₜ Y) {s : Set X} : IsOpen (h '' s) ↔ IsOpen s

Full source

@[simp]
theorem isOpen_image (h : X ≃ₜ Y) {s : Set X} : IsOpenIsOpen (h '' s) ↔ IsOpen s := by
  rw [← preimage_symm, isOpen_preimage]

Openness Criterion for Images under Homeomorphisms

Informal description

For a homeomorphism $h \colon X \simeq_{\text{top}} Y$ between topological spaces $X$ and $Y$, and any subset $s \subseteq X$, the image $h(s)$ is open in $Y$ if and only if $s$ is open in $X$.

Homeomorph.isOpenMap theorem

(h : X ≃ₜ Y) : IsOpenMap h

Full source

protected theorem isOpenMap (h : X ≃ₜ Y) : IsOpenMap h := fun _ => h.isOpen_image.2

Homeomorphisms are Open Maps

Informal description

For any homeomorphism $h \colon X \simeq_{\text{top}} Y$ between topological spaces $X$ and $Y$, the function $h$ is an open map. That is, for every open subset $U \subseteq X$, the image $h(U)$ is open in $Y$.

Homeomorph.isOpenQuotientMap theorem

(h : X ≃ₜ Y) : IsOpenQuotientMap h

Full source

protected theorem isOpenQuotientMap (h : X ≃ₜ Y) : IsOpenQuotientMap h :=
  ⟨h.surjective, h.continuous, h.isOpenMap⟩

Homeomorphisms are Open Quotient Maps

Informal description

For any homeomorphism $h \colon X \simeq_{\text{top}} Y$ between topological spaces $X$ and $Y$, the map $h$ is an open quotient map. That is, $h$ is a surjective continuous open map.

Homeomorph.isClosed_preimage theorem

(h : X ≃ₜ Y) {s : Set Y} : IsClosed (h ⁻¹' s) ↔ IsClosed s

Full source

@[simp]
theorem isClosed_preimage (h : X ≃ₜ Y) {s : Set Y} : IsClosedIsClosed (h ⁻¹' s) ↔ IsClosed s := by
  simp only [← isOpen_compl_iff, ← preimage_compl, isOpen_preimage]

Homeomorphism Preserves Closed Sets via Preimage

Informal description

Let $X$ and $Y$ be topological spaces, and let $h : X \simeq Y$ be a homeomorphism between them. For any subset $s \subseteq Y$, the preimage $h^{-1}(s)$ is closed in $X$ if and only if $s$ is closed in $Y$.

Homeomorph.isClosed_image theorem

(h : X ≃ₜ Y) {s : Set X} : IsClosed (h '' s) ↔ IsClosed s

Full source

@[simp]
theorem isClosed_image (h : X ≃ₜ Y) {s : Set X} : IsClosedIsClosed (h '' s) ↔ IsClosed s := by
  rw [← preimage_symm, isClosed_preimage]

Homeomorphism Preserves Closed Sets via Image

Informal description

Let $X$ and $Y$ be topological spaces and $h \colon X \simeq Y$ be a homeomorphism. For any subset $s \subseteq X$, the image $h(s)$ is closed in $Y$ if and only if $s$ is closed in $X$.

Homeomorph.isClosedMap theorem

(h : X ≃ₜ Y) : IsClosedMap h

Full source

protected theorem isClosedMap (h : X ≃ₜ Y) : IsClosedMap h := fun _ => h.isClosed_image.2

Homeomorphisms are closed maps

Informal description

Let $X$ and $Y$ be topological spaces and $h \colon X \simeq Y$ be a homeomorphism. Then $h$ is a closed map, meaning that for every closed subset $U \subseteq X$, the image $h(U)$ is closed in $Y$.

Homeomorph.isOpenEmbedding theorem

(h : X ≃ₜ Y) : IsOpenEmbedding h

Full source

theorem isOpenEmbedding (h : X ≃ₜ Y) : IsOpenEmbedding h :=
  .of_isEmbedding_isOpenMap h.isEmbedding h.isOpenMap

Homeomorphisms are Open Embeddings

Informal description

For any homeomorphism $h \colon X \simeq_{\text{top}} Y$ between topological spaces $X$ and $Y$, the function $h$ is an open embedding. That is, $h$ is injective, continuous, and maps open subsets of $X$ to open subsets of $Y$, while also inducing the topology on $X$ from $Y$.

Homeomorph.isClosedEmbedding theorem

(h : X ≃ₜ Y) : IsClosedEmbedding h

Full source

theorem isClosedEmbedding (h : X ≃ₜ Y) : IsClosedEmbedding h :=
  .of_isEmbedding_isClosedMap h.isEmbedding h.isClosedMap

Homeomorphisms are Closed Embeddings

Informal description

For any homeomorphism $h \colon X \simeq_{\text{top}} Y$ between topological spaces $X$ and $Y$, the function $h$ is a closed embedding. That is, $h$ is injective, continuous, and maps closed subsets of $X$ to closed subsets of $Y$, while also inducing the topology on $X$ from $Y$.

Homeomorph.preimage_closure theorem

(h : X ≃ₜ Y) (s : Set Y) : h ⁻¹' closure s = closure (h ⁻¹' s)

Full source

theorem preimage_closure (h : X ≃ₜ Y) (s : Set Y) : h ⁻¹' closure s = closure (h ⁻¹' s) :=
  h.isOpenMap.preimage_closure_eq_closure_preimage h.continuous _

Homeomorphism Preserves Closure Preimage

Informal description

For any homeomorphism $h \colon X \simeq_{\text{top}} Y$ between topological spaces $X$ and $Y$, and any subset $s \subseteq Y$, the preimage of the closure of $s$ under $h$ equals the closure of the preimage of $s$, i.e., \[ h^{-1}(\overline{s}) = \overline{h^{-1}(s)}. \]

Homeomorph.image_closure theorem

(h : X ≃ₜ Y) (s : Set X) : h '' closure s = closure (h '' s)

Full source

theorem image_closure (h : X ≃ₜ Y) (s : Set X) : h '' closure s = closure (h '' s) := by
  rw [← preimage_symm, preimage_closure]

Homeomorphism Preserves Closure Image

Informal description

For any homeomorphism $h \colon X \simeq_{\text{top}} Y$ between topological spaces $X$ and $Y$, and any subset $s \subseteq X$, the image of the closure of $s$ under $h$ equals the closure of the image of $s$, i.e., \[ h(\overline{s}) = \overline{h(s)}. \]

Homeomorph.preimage_interior theorem

(h : X ≃ₜ Y) (s : Set Y) : h ⁻¹' interior s = interior (h ⁻¹' s)

Full source

theorem preimage_interior (h : X ≃ₜ Y) (s : Set Y) : h ⁻¹' interior s = interior (h ⁻¹' s) :=
  h.isOpenMap.preimage_interior_eq_interior_preimage h.continuous _

Preimage of Interior under Homeomorphism Equals Interior of Preimage

Informal description

Let $h \colon X \simeq_{\text{top}} Y$ be a homeomorphism between topological spaces $X$ and $Y$. For any subset $s \subseteq Y$, the preimage of the interior of $s$ under $h$ equals the interior of the preimage of $s$, i.e., \[ h^{-1}(\text{int}(s)) = \text{int}(h^{-1}(s)). \]

Homeomorph.image_interior theorem

(h : X ≃ₜ Y) (s : Set X) : h '' interior s = interior (h '' s)

Full source

theorem image_interior (h : X ≃ₜ Y) (s : Set X) : h '' interior s = interior (h '' s) := by
  rw [← preimage_symm, preimage_interior]

Image of Interior under Homeomorphism Equals Interior of Image

Informal description

Let $h \colon X \simeq_{\text{top}} Y$ be a homeomorphism between topological spaces $X$ and $Y$. For any subset $s \subseteq X$, the image of the interior of $s$ under $h$ equals the interior of the image of $s$, i.e., \[ h(\text{int}(s)) = \text{int}(h(s)). \]

Homeomorph.preimage_frontier theorem

(h : X ≃ₜ Y) (s : Set Y) : h ⁻¹' frontier s = frontier (h ⁻¹' s)

Full source

theorem preimage_frontier (h : X ≃ₜ Y) (s : Set Y) : h ⁻¹' frontier s = frontier (h ⁻¹' s) :=
  h.isOpenMap.preimage_frontier_eq_frontier_preimage h.continuous _

Preimage of Frontier under Homeomorphism Equals Frontier of Preimage

Informal description

Let $h \colon X \simeq_{\text{top}} Y$ be a homeomorphism between topological spaces $X$ and $Y$. For any subset $s \subseteq Y$, the preimage of the frontier of $s$ under $h$ equals the frontier of the preimage of $s$, i.e., \[ h^{-1}(\partial s) = \partial h^{-1}(s). \]

Homeomorph.image_frontier theorem

(h : X ≃ₜ Y) (s : Set X) : h '' frontier s = frontier (h '' s)

Full source

theorem image_frontier (h : X ≃ₜ Y) (s : Set X) : h '' frontier s = frontier (h '' s) := by
  rw [← preimage_symm, preimage_frontier]

Image of Frontier under Homeomorphism Equals Frontier of Image

Informal description

Let $h \colon X \simeq_{\text{top}} Y$ be a homeomorphism between topological spaces $X$ and $Y$. For any subset $s \subseteq X$, the image of the frontier of $s$ under $h$ equals the frontier of the image of $s$, i.e., \[ h(\partial s) = \partial h(s). \]

Homeomorph.comp_continuous_iff theorem

(h : X ≃ₜ Y) {f : Z → X} : Continuous (h ∘ f) ↔ Continuous f

Full source

@[simp]
theorem comp_continuous_iff (h : X ≃ₜ Y) {f : Z → X} : ContinuousContinuous (h ∘ f) ↔ Continuous f :=
  h.isInducing.continuous_iff.symm

Continuity of Composition with Homeomorphism

Informal description

Let $h \colon X \simeq_{\text{top}} Y$ be a homeomorphism between topological spaces $X$ and $Y$. For any function $f \colon Z \to X$, the composition $h \circ f$ is continuous if and only if $f$ is continuous.

Homeomorph.comp_continuous_iff' theorem

(h : X ≃ₜ Y) {f : Y → Z} : Continuous (f ∘ h) ↔ Continuous f

Full source

@[simp]
theorem comp_continuous_iff' (h : X ≃ₜ Y) {f : Y → Z} : ContinuousContinuous (f ∘ h) ↔ Continuous f :=
  h.isQuotientMap.continuous_iff.symm

Continuity of Composition with Homeomorphism Inverse

Informal description

Let $h \colon X \simeq_{\text{top}} Y$ be a homeomorphism between topological spaces $X$ and $Y$. For any function $f \colon Y \to Z$, the composition $f \circ h \colon X \to Z$ is continuous if and only if $f$ is continuous.

Homeomorph.comp_continuousAt_iff theorem

(h : X ≃ₜ Y) (f : Z → X) (z : Z) : ContinuousAt (h ∘ f) z ↔ ContinuousAt f z

Full source

theorem comp_continuousAt_iff (h : X ≃ₜ Y) (f : Z → X) (z : Z) :
    ContinuousAtContinuousAt (h ∘ f) z ↔ ContinuousAt f z :=
  h.isInducing.continuousAt_iff.symm

Continuity of Composition with Homeomorphism at a Point

Informal description

Let $h \colon X \simeq_{\text{top}} Y$ be a homeomorphism between topological spaces $X$ and $Y$, and let $f \colon Z \to X$ be a function from a topological space $Z$ to $X$. For any point $z \in Z$, the composition $h \circ f$ is continuous at $z$ if and only if $f$ is continuous at $z$.

Homeomorph.comp_continuousAt_iff' theorem

(h : X ≃ₜ Y) (f : Y → Z) (x : X) : ContinuousAt (f ∘ h) x ↔ ContinuousAt f (h x)

Full source

theorem comp_continuousAt_iff' (h : X ≃ₜ Y) (f : Y → Z) (x : X) :
    ContinuousAtContinuousAt (f ∘ h) x ↔ ContinuousAt f (h x) :=
  h.isInducing.continuousAt_iff' (by simp)

Continuity of Composition with Homeomorphism at a Point

Informal description

Let $h \colon X \simeq_{\text{top}} Y$ be a homeomorphism between topological spaces $X$ and $Y$, and let $f \colon Y \to Z$ be a function. For any point $x \in X$, the composition $f \circ h$ is continuous at $x$ if and only if $f$ is continuous at $h(x) \in Y$.

Homeomorph.comp_isOpenMap_iff theorem

(h : X ≃ₜ Y) {f : Z → X} : IsOpenMap (h ∘ f) ↔ IsOpenMap f

Full source

@[simp]
theorem comp_isOpenMap_iff (h : X ≃ₜ Y) {f : Z → X} : IsOpenMapIsOpenMap (h ∘ f) ↔ IsOpenMap f := by
  refine ⟨?_, fun hf => h.isOpenMap.comp hf⟩
  intro hf
  rw [← Function.id_comp f, ← h.symm_comp_self, Function.comp_assoc]
  exact h.symm.isOpenMap.comp hf

Composition with Homeomorphism Preserves Open Maps: $h \circ f$ is open $\leftrightarrow$ $f$ is open

Informal description

Let $h \colon X \simeq_{\text{top}} Y$ be a homeomorphism between topological spaces $X$ and $Y$, and let $f \colon Z \to X$ be a function. The composition $h \circ f$ is an open map if and only if $f$ is an open map.

Homeomorph.comp_isOpenMap_iff' theorem

(h : X ≃ₜ Y) {f : Y → Z} : IsOpenMap (f ∘ h) ↔ IsOpenMap f

Full source

@[simp]
theorem comp_isOpenMap_iff' (h : X ≃ₜ Y) {f : Y → Z} : IsOpenMapIsOpenMap (f ∘ h) ↔ IsOpenMap f := by
  refine ⟨?_, fun hf => hf.comp h.isOpenMap⟩
  intro hf
  rw [← Function.comp_id f, ← h.self_comp_symm, ← Function.comp_assoc]
  exact hf.comp h.symm.isOpenMap

Open Map Property of Composition with Homeomorphism: $f \circ h$ is Open if and only if $f$ is Open

Informal description

Let $h \colon X \simeq_{\text{top}} Y$ be a homeomorphism between topological spaces $X$ and $Y$, and let $f \colon Y \to Z$ be a function. Then the composition $f \circ h$ is an open map if and only if $f$ is an open map.

Homeomorph.homeomorphOfUnique definition

[Unique X] [Unique Y] : X ≃ₜ Y

Full source

/-- If both `X` and `Y` have a unique element, then `X ≃ₜ Y`. -/
@[simps!]
def homeomorphOfUnique [Unique X] [Unique Y] : X ≃ₜ Y :=
  { Equiv.ofUnique X Y with
    continuous_toFun := continuous_const
    continuous_invFun := continuous_const }

Homeomorphism between uniquely inhabited topological spaces

Informal description

Given two topological spaces $X$ and $Y$ each with a unique element, there exists a homeomorphism between them. The homeomorphism maps the unique element of $X$ to the unique element of $Y$ and vice versa, with both the function and its inverse being continuous (which is automatically satisfied since all functions between singleton spaces are continuous).

Homeomorph.map_nhds_eq theorem

(h : X ≃ₜ Y) (x : X) : map h (𝓝 x) = 𝓝 (h x)

Full source

@[simp]
theorem map_nhds_eq (h : X ≃ₜ Y) (x : X) : map h (𝓝 x) = 𝓝 (h x) :=
  h.isEmbedding.map_nhds_of_mem _ (by simp)

Homeomorphism Preserves Neighborhood Filters

Informal description

For any homeomorphism $h \colon X \simeq_{\text{top}} Y$ between topological spaces $X$ and $Y$, and for any point $x \in X$, the pushforward of the neighborhood filter $\mathcal{N}_x$ under $h$ equals the neighborhood filter $\mathcal{N}_{h(x)}$ at $h(x)$ in $Y$. That is, $h_*(\mathcal{N}_x) = \mathcal{N}_{h(x)}$.

Homeomorph.symm_map_nhds_eq theorem

(h : X ≃ₜ Y) (x : X) : map h.symm (𝓝 (h x)) = 𝓝 x

Full source

theorem symm_map_nhds_eq (h : X ≃ₜ Y) (x : X) : map h.symm (𝓝 (h x)) = 𝓝 x := by
  rw [h.symm.map_nhds_eq, h.symm_apply_apply]

Inverse Homeomorphism Preserves Neighborhood Filters: $h^{-1}_*(\mathcal{N}_{h(x)}) = \mathcal{N}_x$

Informal description

For any homeomorphism $h \colon X \simeq_{\text{top}} Y$ between topological spaces $X$ and $Y$, and for any point $x \in X$, the pushforward of the neighborhood filter $\mathcal{N}_{h(x)}$ under the inverse homeomorphism $h^{-1}$ equals the neighborhood filter $\mathcal{N}_x$ at $x$ in $X$. That is, $h^{-1}_*(\mathcal{N}_{h(x)}) = \mathcal{N}_x$.

Homeomorph.nhds_eq_comap theorem

(h : X ≃ₜ Y) (x : X) : 𝓝 x = comap h (𝓝 (h x))

Full source

theorem nhds_eq_comap (h : X ≃ₜ Y) (x : X) : 𝓝 x = comap h (𝓝 (h x)) :=
  h.isInducing.nhds_eq_comap x

Neighborhood Filter Characterization via Homeomorphism Preimage

Informal description

For any homeomorphism $h \colon X \simeq_{\text{top}} Y$ between topological spaces $X$ and $Y$, and for any point $x \in X$, the neighborhood filter $\mathcal{N}_x$ of $x$ in $X$ is equal to the preimage under $h$ of the neighborhood filter $\mathcal{N}_{h(x)}$ of $h(x)$ in $Y$, i.e., $\mathcal{N}_x = h^{-1}(\mathcal{N}_{h(x)})$.

Homeomorph.comap_nhds_eq theorem

(h : X ≃ₜ Y) (y : Y) : comap h (𝓝 y) = 𝓝 (h.symm y)

Full source

@[simp]
theorem comap_nhds_eq (h : X ≃ₜ Y) (y : Y) : comap h (𝓝 y) = 𝓝 (h.symm y) := by
  rw [h.nhds_eq_comap, h.apply_symm_apply]

Preimage of Neighborhood Filter under Homeomorphism Equals Neighborhood Filter of Inverse Point

Informal description

For any homeomorphism $h \colon X \simeq_{\text{top}} Y$ between topological spaces $X$ and $Y$, and for any point $y \in Y$, the preimage of the neighborhood filter $\mathcal{N}_y$ under $h$ is equal to the neighborhood filter $\mathcal{N}_{h^{-1}(y)}$ of the inverse image $h^{-1}(y)$ in $X$, i.e., $h^{-1}(\mathcal{N}_y) = \mathcal{N}_{h^{-1}(y)}$.

Equiv.toHomeomorph definition

(e : X ≃ Y) (he : ∀ s, IsOpen (e ⁻¹' s) ↔ IsOpen s) : X ≃ₜ Y

Full source

/-- An equivalence between topological spaces respecting openness is a homeomorphism. -/
@[simps toEquiv]
def toHomeomorph (e : X ≃ Y) (he : ∀ s, IsOpenIsOpen (e ⁻¹' s) ↔ IsOpen s) : X ≃ₜ Y where
  toEquiv := e
  continuous_toFun := continuous_def.2 fun _ ↦ (he _).2
  continuous_invFun := continuous_def.2 fun s ↦ by convert (he _).1; simp

Homeomorphism induced by an open-preserving equivalence

Informal description

Given a bijection $e : X \to Y$ between topological spaces, if for every subset $s \subseteq Y$ the preimage $e^{-1}(s)$ is open in $X$ if and only if $s$ is open in $Y$, then $e$ induces a homeomorphism between $X$ and $Y$.

Equiv.coe_toHomeomorph theorem

(e : X ≃ Y) (he) : ⇑(e.toHomeomorph he) = e

Full source

@[simp] lemma coe_toHomeomorph (e : X ≃ Y) (he) : ⇑(e.toHomeomorph he) = e := rfl

Homeomorphism Construction Preserves Underlying Function

Informal description

For any bijection $e : X \to Y$ between topological spaces and any proof $he$ that $e$ preserves open sets (i.e., for any subset $s \subseteq Y$, $e^{-1}(s)$ is open in $X$ if and only if $s$ is open in $Y$), the underlying function of the homeomorphism constructed from $e$ via `toHomeomorph` is equal to $e$ itself. In other words, $\text{toHomeomorph}(e, he) = e$ as functions.

Equiv.toHomeomorph_apply theorem

(e : X ≃ Y) (he) (x : X) : e.toHomeomorph he x = e x

Full source

lemma toHomeomorph_apply (e : X ≃ Y) (he) (x : X) : e.toHomeomorph he x = e x := rfl

Homeomorphism Application Equals Bijection Application

Informal description

For any bijection $e : X \to Y$ between topological spaces that induces a homeomorphism (i.e., satisfies $\forall s, \text{IsOpen}(e^{-1}(s)) \leftrightarrow \text{IsOpen}(s)$), and for any point $x \in X$, the homeomorphism $e.toHomeomorph$ applied to $x$ equals $e(x)$.

Equiv.toHomeomorph_refl theorem

: (Equiv.refl X).toHomeomorph (fun _s ↦ Iff.rfl) = Homeomorph.refl _

Full source

@[simp] lemma toHomeomorph_refl :
  (Equiv.refl X).toHomeomorph (fun _s ↦ Iff.rfl) = Homeomorph.refl _ := rfl

Identity Equivalence Yields Identity Homeomorphism

Informal description

The homeomorphism induced by the identity equivalence on a topological space $X$ is equal to the identity homeomorphism on $X$.

Equiv.toHomeomorph_symm theorem

(e : X ≃ Y) (he) : (e.toHomeomorph he).symm = e.symm.toHomeomorph fun s ↦ by convert (he _).symm; simp

Full source

@[simp] lemma toHomeomorph_symm (e : X ≃ Y) (he) :
  (e.toHomeomorph he).symm = e.symm.toHomeomorph fun s ↦ by convert (he _).symm; simp := rfl

Inverse of Induced Homeomorphism Equals Homeomorphism of Inverse

Informal description

Let $X$ and $Y$ be topological spaces, and let $e : X \to Y$ be a bijection such that for every subset $s \subseteq Y$, the preimage $e^{-1}(s)$ is open in $X$ if and only if $s$ is open in $Y$. Then the inverse of the homeomorphism induced by $e$ equals the homeomorphism induced by the inverse bijection $e^{-1} : Y \to X$.

Equiv.toHomeomorph_trans theorem

 (e : X ≃ Y) (f : Y ≃ Z) (he hf) :
  (e.trans f).toHomeomorph (fun _s ↦ (he _).trans (hf _)) = (e.toHomeomorph he).trans (f.toHomeomorph hf)

Full source

lemma toHomeomorph_trans (e : X ≃ Y) (f : Y ≃ Z) (he hf) :
    (e.trans f).toHomeomorph (fun _s ↦ (he _).trans (hf _)) =
    (e.toHomeomorph he).trans (f.toHomeomorph hf) := rfl

Composition of Induced Homeomorphisms Equals Homeomorphism of Composition

Informal description

Let $X$, $Y$, and $Z$ be topological spaces, and let $e : X \simeq Y$ and $f : Y \simeq Z$ be bijections such that: 1. For every subset $s \subseteq Y$, the preimage $e^{-1}(s)$ is open in $X$ if and only if $s$ is open in $Y$ (denoted by `he`). 2. For every subset $s \subseteq Z$, the preimage $f^{-1}(s)$ is open in $Y$ if and only if $s$ is open in $Z$ (denoted by `hf`). Then the homeomorphism induced by the composition $f \circ e : X \simeq Z$ is equal to the composition of the homeomorphisms induced by $e$ and $f$.

Equiv.toHomeomorphOfIsInducing definition

(f : X ≃ Y) (hf : IsInducing f) : X ≃ₜ Y

Full source

/-- An inducing equiv between topological spaces is a homeomorphism. -/
@[simps toEquiv]
def toHomeomorphOfIsInducing (f : X ≃ Y) (hf : IsInducing f) : X ≃ₜ Y :=
  { f with
    continuous_toFun := hf.continuous
    continuous_invFun := hf.continuous_iff.2 <| by simpa using continuous_id }

Homeomorphism from inducing equivalence

Informal description

Given a bijection $f : X \to Y$ between topological spaces, if $f$ is inducing (i.e., the topology on $X$ is the one induced by $f$ from $Y$), then $f$ is a homeomorphism between $X$ and $Y$.

Equiv.toHomeomorphOfContinuousOpen definition

(e : X ≃ Y) (h₁ : Continuous e) (h₂ : IsOpenMap e) : X ≃ₜ Y

Full source

/-- If a bijective map `e : X ≃ Y` is continuous and open, then it is a homeomorphism. -/
@[simps! toEquiv]
def toHomeomorphOfContinuousOpen (e : X ≃ Y) (h₁ : Continuous e) (h₂ : IsOpenMap e) : X ≃ₜ Y :=
  e.toHomeomorphOfIsInducing <|
    IsOpenEmbedding.of_continuous_injective_isOpenMap h₁ e.injective h₂ |>.toIsInducing

Homeomorphism from continuous open bijection

Informal description

Given a bijection $e \colon X \to Y$ between topological spaces, if $e$ is continuous and an open map, then $e$ is a homeomorphism between $X$ and $Y$.

Equiv.toHomeomorphOfContinuousOpen_apply theorem

(e : X ≃ Y) (h₁ : Continuous e) (h₂ : IsOpenMap e) : ⇑(e.toHomeomorphOfContinuousOpen h₁ h₂) = e

Full source

@[simp]
theorem toHomeomorphOfContinuousOpen_apply (e : X ≃ Y) (h₁ : Continuous e) (h₂ : IsOpenMap e) :
    ⇑(e.toHomeomorphOfContinuousOpen h₁ h₂) = e := rfl

Underlying Function of Homeomorphism from Continuous Open Bijection

Informal description

Given a bijection $e \colon X \to Y$ between topological spaces, if $e$ is continuous and an open map, then the underlying function of the homeomorphism constructed from $e$ via `toHomeomorphOfContinuousOpen` is equal to $e$ itself.

Equiv.toHomeomorphOfContinuousOpen_symm_apply theorem

(e : X ≃ Y) (h₁ : Continuous e) (h₂ : IsOpenMap e) : ⇑(e.toHomeomorphOfContinuousOpen h₁ h₂).symm = e.symm

Full source

@[simp]
theorem toHomeomorphOfContinuousOpen_symm_apply (e : X ≃ Y) (h₁ : Continuous e) (h₂ : IsOpenMap e) :
    ⇑(e.toHomeomorphOfContinuousOpen h₁ h₂).symm = e.symm := rfl

Inverse of Homeomorphism from Continuous Open Bijection Equals Inverse of Original Map

Informal description

For any bijection $e \colon X \to Y$ between topological spaces, if $e$ is continuous and an open map, then the inverse of the homeomorphism constructed from $e$ is equal to the inverse of $e$ as a function. That is, $(e.toHomeomorphOfContinuousOpen\, h₁\, h₂)^{-1} = e^{-1}$.

Equiv.toHomeomorphOfContinuousClosed definition

(e : X ≃ Y) (h₁ : Continuous e) (h₂ : IsClosedMap e) : X ≃ₜ Y

Full source

/-- If a bijective map `e : X ≃ Y` is continuous and open, then it is a homeomorphism. -/
@[simps! toEquiv]
def toHomeomorphOfContinuousClosed (e : X ≃ Y) (h₁ : Continuous e) (h₂ : IsClosedMap e) : X ≃ₜ Y :=
  e.toHomeomorphOfIsInducing <|
    IsClosedEmbedding.of_continuous_injective_isClosedMap h₁ e.injective h₂ |>.toIsInducing

Homeomorphism from continuous closed bijection

Informal description

Given a bijection $e \colon X \to Y$ between topological spaces, if $e$ is continuous and a closed map, then $e$ is a homeomorphism between $X$ and $Y$.

Equiv.toHomeomorphOfContinuousClosed_apply theorem

(e : X ≃ Y) (h₁ : Continuous e) (h₂ : IsClosedMap e) : ⇑(e.toHomeomorphOfContinuousClosed h₁ h₂) = e

Full source

@[simp]
theorem toHomeomorphOfContinuousClosed_apply (e : X ≃ Y) (h₁ : Continuous e) (h₂ : IsClosedMap e) :
    ⇑(e.toHomeomorphOfContinuousClosed h₁ h₂) = e := rfl

Underlying Function of Constructed Homeomorphism from Continuous Closed Bijection

Informal description

Let $X$ and $Y$ be topological spaces, and let $e \colon X \to Y$ be a bijection. If $e$ is continuous and a closed map, then the underlying function of the homeomorphism constructed from $e$ (via `toHomeomorphOfContinuousClosed`) coincides with $e$ itself.

Equiv.toHomeomorphOfContinuousClosed_symm_apply theorem

 (e : X ≃ Y) (h₁ : Continuous e) (h₂ : IsClosedMap e) : ⇑(e.toHomeomorphOfContinuousClosed h₁ h₂).symm = e.symm

Full source

@[simp]
theorem toHomeomorphOfContinuousClosed_symm_apply
    (e : X ≃ Y) (h₁ : Continuous e) (h₂ : IsClosedMap e) :
    ⇑(e.toHomeomorphOfContinuousClosed h₁ h₂).symm = e.symm := rfl

Inverse of Homeomorphism from Continuous Closed Bijection Equals Bijection's Inverse

Informal description

Given a bijection $e \colon X \to Y$ between topological spaces, if $e$ is continuous and a closed map, then the inverse of the homeomorphism constructed from $e$ is equal to the inverse of $e$ as a function. That is, $(e.toHomeomorphOfContinuousClosed\, h₁\, h₂)^{-1} = e^{-1}$.

HomeomorphClass structure

(F : Type*) (A B : outParam Type*) [TopologicalSpace A] [TopologicalSpace B] [h : EquivLike F A B]

Full source

/-- `HomeomorphClass F A B` states that `F` is a type of homeomorphisms. -/
class HomeomorphClass (F : Type*) (A B : outParam Type*)
    [TopologicalSpace A] [TopologicalSpace B] [h : EquivLike F A B] : Prop where
  map_continuous : ∀ (f : F), Continuous f
  inv_continuous : ∀ (f : F), Continuous (h.inv f)

Homeomorphism Class

Informal description

The class `HomeomorphClass F A B` states that `F` is a type of homeomorphisms between topological spaces `A` and `B`. A homeomorphism is a bijection that is continuous in both directions, meaning both the function and its inverse are continuous. This class extends `EquivLike`, ensuring that terms of type `F` can be coerced to bijections between `A` and `B`.

HomeomorphClass.toHomeomorph definition

[h : HomeomorphClass F α β] (f : F) : α ≃ₜ β

Full source

/-- Turn an element of a type `F` satisfying `HomeomorphClass F α β` into an actual
`Homeomorph`. This is declared as the default coercion from `F` to `α ≃ₜ β`. -/
@[coe]
def toHomeomorph [h : HomeomorphClass F α β] (f : F) : α ≃ₜ β :=
  { (f : α ≃ β) with
    continuous_toFun := h.map_continuous f
    continuous_invFun := h.inv_continuous f }

Conversion from Homeomorphism Class to explicit homeomorphism

Informal description

Given a type `F` that satisfies `HomeomorphClass F α β` (i.e., elements of `F` represent homeomorphisms between topological spaces `α` and `β`), the function `HomeomorphClass.toHomeomorph` converts an element `f : F` into an explicit homeomorphism `α ≃ₜ β`. This homeomorphism consists of: - A bijection `f : α → β` that is continuous, - An inverse bijection `f⁻¹ : β → α` that is also continuous. This is declared as the default coercion from `F` to `α ≃ₜ β`.

HomeomorphClass.coe_coe theorem

[h : HomeomorphClass F α β] (f : F) : ⇑(h.toHomeomorph f) = ⇑f

Full source

@[simp]
theorem coe_coe [h : HomeomorphClass F α β] (f : F) : ⇑(h.toHomeomorph f) = ⇑f := rfl

Coercion Consistency for Homeomorphism Class

Informal description

For any type `F` that satisfies `HomeomorphClass F α β` (i.e., elements of `F` represent homeomorphisms between topological spaces `α` and `β`), and for any element `f : F`, the underlying function of the homeomorphism obtained via `HomeomorphClass.toHomeomorph f` is equal to the underlying function of `f` itself. In other words, the coercion to a function commutes with the conversion to a homeomorphism.

HomeomorphClass.instCoeOutHomeomorph instance

[HomeomorphClass F α β] : CoeOut F (α ≃ₜ β)

Full source

instance [HomeomorphClass F α β] : CoeOut F (α ≃ₜ β) :=
  ⟨HomeomorphClass.toHomeomorph⟩

Canonical Coercion from Homeomorphism Class to Homeomorphisms

Informal description

For any type `F` that is a homeomorphism class between topological spaces `α` and `β`, there is a canonical coercion from `F` to the type of homeomorphisms `α ≃ₜ β`.

HomeomorphClass.toHomeomorph_injective theorem

[HomeomorphClass F α β] : Function.Injective ((↑) : F → α ≃ₜ β)

Full source

theorem toHomeomorph_injective [HomeomorphClass F α β] : Function.Injective ((↑) : F → α ≃ₜ β) :=
  fun _ _ e ↦ DFunLike.ext _ _ fun a ↦ congr_arg (fun e : α ≃ₜ β ↦ e.toFun a) e

Injectivity of the Homeomorphism Class to Homeomorphism Map

Informal description

For any type `F` that is a homeomorphism class between topological spaces `α` and `β`, the canonical map from `F` to the type of homeomorphisms `α ≃ₜ β` is injective. That is, if two elements of `F` are mapped to the same homeomorphism, then they are equal.

HomeomorphClass.instContinuousMapClass instance

[HomeomorphClass F α β] : ContinuousMapClass F α β

Full source

instance [HomeomorphClass F α β] : ContinuousMapClass F α β where
  map_continuous  f := map_continuous f

Homeomorphism Class as Continuous Map Class

Informal description

For any type `F` that is a homeomorphism class between topological spaces `α` and `β`, every element of `F` can be treated as a continuous map from `α` to `β`.

HomeomorphClass.instHomeomorph instance

: HomeomorphClass (α ≃ₜ β) α β

Full source

instance : HomeomorphClass (α ≃ₜ β) α β where
  map_continuous e := e.continuous_toFun
  inv_continuous e := e.continuous_invFun

Homeomorphism Class Structure on Homeomorphisms

Informal description

The type of homeomorphisms $\alpha \simeqₜ \beta$ between topological spaces $\alpha$ and $\beta$ forms a homeomorphism class, meaning every element in this type can be treated as a homeomorphism between $\alpha$ and $\beta$.

IsHomeomorph structure

(f : X → Y)

Full source

/-- 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`. -/
structure IsHomeomorph (f : X → Y) : Prop where
  continuous : Continuous f
  isOpenMap : IsOpenMap f
  bijective : Function.Bijective f

Homeomorphism predicate

Informal description

The predicate `IsHomeomorph f` asserts that a function $f : X \to Y$ between topological spaces is a homeomorphism, meaning it is a continuous bijection with a continuous inverse. This is stronger than merely being a continuous bijection, as it also requires $f$ to be an open map (or equivalently, a closed map).

Homeomorph.isHomeomorph theorem

(h : X ≃ₜ Y) : IsHomeomorph h

Full source

protected theorem Homeomorph.isHomeomorph (h : X ≃ₜ Y) : IsHomeomorph h :=
  ⟨h.continuous, h.isOpenMap, h.bijective⟩

Homeomorphism Satisfies Homeomorphism Predicate

Informal description

For any homeomorphism $h \colon X \simeq_{\text{top}} Y$ between topological spaces $X$ and $Y$, the function $h$ satisfies the homeomorphism predicate, meaning it is a continuous bijection with a continuous inverse.

IsHomeomorph.injective theorem

(hf : IsHomeomorph f) : Function.Injective f

Full source

protected lemma injective (hf : IsHomeomorph f) : Function.Injective f := hf.bijective.injective

Injectivity of Homeomorphisms

Informal description

If a function $f : X \to Y$ between topological spaces is a homeomorphism, then $f$ is injective.

IsHomeomorph.surjective theorem

(hf : IsHomeomorph f) : Function.Surjective f

Full source

protected lemma surjective (hf : IsHomeomorph f) : Function.Surjective f := hf.bijective.surjective

Homeomorphisms are surjective

Informal description

If a function $f : X \to Y$ between topological spaces is a homeomorphism, then $f$ is surjective.

IsHomeomorph.id theorem

: IsHomeomorph (@id X)

Full source

protected lemma id : IsHomeomorph (@id X) := ⟨continuous_id, .id, Function.bijective_id⟩

Identity Function is a Homeomorphism

Informal description

The identity function $\mathrm{id} : X \to X$ on a topological space $X$ is a homeomorphism.

IsHomeomorph.comp theorem

{g : Y → Z} (hg : IsHomeomorph g) (hf : IsHomeomorph f) : IsHomeomorph (g ∘ f)

Full source

lemma comp {g : Y → Z} (hg : IsHomeomorph g) (hf : IsHomeomorph f) : IsHomeomorph (g ∘ f) :=
  ⟨hg.1.comp hf.1, hg.2.comp hf.2, hg.3.comp hf.3⟩

Composition of Homeomorphisms is a Homeomorphism

Informal description

Let $X$, $Y$, and $Z$ be topological spaces, and let $f \colon X \to Y$ and $g \colon Y \to Z$ be homeomorphisms. Then the composition $g \circ f \colon X \to Z$ is also a homeomorphism.

Main definitions and results