doc-next-gen

Mathlib.Topology.Homeomorph.Lemmas

Module docstring

{"# Further properties of homeomorphisms

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

"}

Topology.IsEmbedding.toHomeomorph definition
{f : X → Y} (hf : IsEmbedding f) : X ≃ₜ Set.range f
Full source 
/-- Homeomorphism given an embedding. -/
@[simps! apply_coe]
noncomputable def _root_.Topology.IsEmbedding.toHomeomorph {f : X → Y} (hf : IsEmbedding f) :
    X ≃ₜ Set.range f :=
  Equiv.ofInjective f hf.injective |>.toHomeomorphOfIsInducing <|
    IsInducing.subtypeVal.of_comp_iff.mp hf.toIsInducing
Homeomorphism induced by a topological embedding
Informal description
Given a topological embedding \( f : X \to Y \), there exists a homeomorphism between \( X \) and the range of \( f \) in \( Y \). This homeomorphism is constructed by restricting the codomain of \( f \) to its range and using the fact that \( f \) is an embedding to ensure continuity in both directions.
Topology.IsEmbedding.toHomeomorphOfSurjective definition
{f : X → Y} (hf : IsEmbedding f) (hsurj : Function.Surjective f) : X ≃ₜ Y
Full source 
/-- A surjective embedding is a homeomorphism. -/
@[simps! apply]
noncomputable def _root_.Topology.IsEmbedding.toHomeomorphOfSurjective {f : X → Y}
    (hf : IsEmbedding f) (hsurj : Function.Surjective f) : X ≃ₜ Y :=
  Equiv.ofBijective f ⟨hf.injective, hsurj⟩ |>.toHomeomorphOfIsInducing hf.toIsInducing
Homeomorphism from a surjective embedding
Informal description
Given a topological embedding \( f : X \to Y \) that is also surjective, the function \( f \) induces a homeomorphism between \( X \) and \( Y \). This is constructed by first obtaining a bijective equivalence from \( f \) (using its injectivity from being an embedding and given surjectivity), then promoting it to a homeomorphism using the fact that \( f \) is inducing.
Homeomorph.secondCountableTopology theorem
[SecondCountableTopology Y] (h : X ≃ₜ Y) : SecondCountableTopology X
Full source 
protected theorem secondCountableTopology [SecondCountableTopology Y]
    (h : X ≃ₜ Y) : SecondCountableTopology X :=
  h.isInducing.secondCountableTopology
Second-Countability is Preserved under Homeomorphism
Informal description
Let $X$ and $Y$ be topological spaces with a homeomorphism $h \colon X \simeq_{\text{top}} Y$. If $Y$ is second-countable, then $X$ is also second-countable.
Homeomorph.isCompact_image theorem
{s : Set X} (h : X ≃ₜ Y) : IsCompact (h '' s) ↔ IsCompact s
Full source 
/-- If `h : X → Y` is a homeomorphism, `h(s)` is compact iff `s` is. -/
@[simp]
theorem isCompact_image {s : Set X} (h : X ≃ₜ Y) : IsCompactIsCompact (h '' s) ↔ IsCompact s :=
  h.isEmbedding.isCompact_iff.symm
Compactness Preservation under Homeomorphism: $h(s)$ Compact $\iff$ $s$ Compact
Informal description
Let $X$ and $Y$ be topological spaces, $h \colon X \to Y$ a homeomorphism, and $s \subseteq X$ a subset. Then the image $h(s)$ is compact in $Y$ if and only if $s$ is compact in $X$.
Homeomorph.isCompact_preimage theorem
{s : Set Y} (h : X ≃ₜ Y) : IsCompact (h ⁻¹' s) ↔ IsCompact s
Full source 
/-- If `h : X → Y` is a homeomorphism, `h⁻¹(s)` is compact iff `s` is. -/
@[simp]
theorem isCompact_preimage {s : Set Y} (h : X ≃ₜ Y) : IsCompactIsCompact (h ⁻¹' s) ↔ IsCompact s := by
  rw [← image_symm]; exact h.symm.isCompact_image
Compactness Preservation under Homeomorphism: $h^{-1}(s)$ Compact $\iff$ $s$ Compact
Informal description
Let $X$ and $Y$ be topological spaces and $h \colon X \to Y$ be a homeomorphism. For any subset $s \subseteq Y$, the preimage $h^{-1}(s)$ is compact in $X$ if and only if $s$ is compact in $Y$.
Homeomorph.isSigmaCompact_image theorem
{s : Set X} (h : X ≃ₜ Y) : IsSigmaCompact (h '' s) ↔ IsSigmaCompact s
Full source 
/-- If `h : X → Y` is a homeomorphism, `s` is σ-compact iff `h(s)` is. -/
@[simp]
theorem isSigmaCompact_image {s : Set X} (h : X ≃ₜ Y) :
    IsSigmaCompactIsSigmaCompact (h '' s) ↔ IsSigmaCompact s :=
  h.isEmbedding.isSigmaCompact_iff.symm
Preservation of $\sigma$-compactness under homeomorphisms
Informal description
Let $X$ and $Y$ be topological spaces, and let $h \colon X \to Y$ be a homeomorphism. For any subset $s \subseteq X$, $s$ is $\sigma$-compact if and only if its image $h(s)$ is $\sigma$-compact.
Homeomorph.isSigmaCompact_preimage theorem
{s : Set Y} (h : X ≃ₜ Y) : IsSigmaCompact (h ⁻¹' s) ↔ IsSigmaCompact s
Full source 
/-- If `h : X → Y` is a homeomorphism, `h⁻¹(s)` is σ-compact iff `s` is. -/
@[simp]
theorem isSigmaCompact_preimage {s : Set Y} (h : X ≃ₜ Y) :
    IsSigmaCompactIsSigmaCompact (h ⁻¹' s) ↔ IsSigmaCompact s := by
  rw [← image_symm]; exact h.symm.isSigmaCompact_image
Preservation of $\sigma$-compactness under homeomorphic preimages
Informal description
Let $X$ and $Y$ be topological spaces and $h \colon X \to Y$ be a homeomorphism. For any subset $s \subseteq Y$, the preimage $h^{-1}(s)$ is $\sigma$-compact if and only if $s$ is $\sigma$-compact.
Homeomorph.isPreconnected_image theorem
{s : Set X} (h : X ≃ₜ Y) : IsPreconnected (h '' s) ↔ IsPreconnected s
Full source 
@[simp]
theorem isPreconnected_image {s : Set X} (h : X ≃ₜ Y) :
    IsPreconnectedIsPreconnected (h '' s) ↔ IsPreconnected s :=
  ⟨fun hs ↦ by simpa only [image_symm, preimage_image]
    using hs.image _ h.symm.continuous.continuousOn,
    fun hs ↦ hs.image _ h.continuous.continuousOn⟩
Preconnectedness is Preserved under Homeomorphic Images
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 $h(s)$ is preconnected if and only if $s$ is preconnected.
Homeomorph.isPreconnected_preimage theorem
{s : Set Y} (h : X ≃ₜ Y) : IsPreconnected (h ⁻¹' s) ↔ IsPreconnected s
Full source 
@[simp]
theorem isPreconnected_preimage {s : Set Y} (h : X ≃ₜ Y) :
    IsPreconnectedIsPreconnected (h ⁻¹' s) ↔ IsPreconnected s := by
  rw [← image_symm, isPreconnected_image]
Preconnectedness is Preserved under Homeomorphic Preimages
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 $h^{-1}(s)$ is preconnected if and only if $s$ is preconnected.
Homeomorph.isConnected_image theorem
{s : Set X} (h : X ≃ₜ Y) : IsConnected (h '' s) ↔ IsConnected s
Full source 
@[simp]
theorem isConnected_image {s : Set X} (h : X ≃ₜ Y) :
    IsConnectedIsConnected (h '' s) ↔ IsConnected s :=
  image_nonempty.and h.isPreconnected_image
Connectedness is Preserved under Homeomorphic Images
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 $h(s)$ is connected if and only if $s$ is connected.
Homeomorph.isConnected_preimage theorem
{s : Set Y} (h : X ≃ₜ Y) : IsConnected (h ⁻¹' s) ↔ IsConnected s
Full source 
@[simp]
theorem isConnected_preimage {s : Set Y} (h : X ≃ₜ Y) :
    IsConnectedIsConnected (h ⁻¹' s) ↔ IsConnected s := by
  rw [← image_symm, isConnected_image]
Connectedness is Preserved under Homeomorphic Preimages
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 $h^{-1}(s)$ is connected if and only if $s$ is connected.
Homeomorph.image_connectedComponentIn theorem
{s : Set X} (h : X ≃ₜ Y) {x : X} (hx : x ∈ s) : h '' connectedComponentIn s x = connectedComponentIn (h '' s) (h x)
Full source 
theorem image_connectedComponentIn {s : Set X} (h : X ≃ₜ Y) {x : X} (hx : x ∈ s) :
    h '' connectedComponentIn s x = connectedComponentIn (h '' s) (h x) := by
  refine (h.continuous.image_connectedComponentIn_subset hx).antisymm ?_
  have := h.symm.continuous.image_connectedComponentIn_subset (mem_image_of_mem h hx)
  rwa [image_subset_iff, h.preimage_symm, h.image_symm, h.preimage_image, h.symm_apply_apply]
    at this
Homeomorphism Preserves Connected Components in Subsets
Informal description
Let $X$ and $Y$ be topological spaces, and let $h \colon X \simeq_{\text{top}} Y$ be a homeomorphism. For any subset $s \subseteq X$ and any point $x \in s$, the image under $h$ of the connected component of $x$ in $s$ equals the connected component of $h(x)$ in $h(s)$. In symbols: \[ h(\text{connectedComponentIn}(s, x)) = \text{connectedComponentIn}(h(s), h(x)). \]
Homeomorph.comap_cocompact theorem
(h : X ≃ₜ Y) : comap h (cocompact Y) = cocompact X
Full source 
@[simp]
theorem comap_cocompact (h : X ≃ₜ Y) : comap h (cocompact Y) = cocompact X :=
  (comap_cocompact_le h.continuous).antisymm <|
    (hasBasis_cocompact.le_basis_iff (hasBasis_cocompact.comap h)).2 fun K hK =>
      ⟨h ⁻¹' K, h.isCompact_preimage.2 hK, Subset.rfl⟩
Homeomorphism Preserves Cocompact Filter via Preimage: $\text{comap}\, h\, (\text{cocompact}\, Y) = \text{cocompact}\, X$
Informal description
For any homeomorphism $h \colon X \simeq_{\text{top}} Y$ between topological spaces $X$ and $Y$, the preimage filter of the cocompact filter on $Y$ under $h$ is equal to the cocompact filter on $X$. In other words, for any subset $s \subseteq Y$, the preimage $h^{-1}(s)$ has a compact complement in $X$ if and only if $s$ has a compact complement in $Y$.
Homeomorph.map_cocompact theorem
(h : X ≃ₜ Y) : map h (cocompact X) = cocompact Y
Full source 
@[simp]
theorem map_cocompact (h : X ≃ₜ Y) : map h (cocompact X) = cocompact Y := by
  rw [← h.comap_cocompact, map_comap_of_surjective h.surjective]
Homeomorphism Preserves Cocompact Filter via Image: $\text{map}\, h\, (\text{cocompact}\, X) = \text{cocompact}\, Y$
Informal description
For any homeomorphism $h \colon X \simeq_{\text{top}} Y$ between topological spaces $X$ and $Y$, the image filter of the cocompact filter on $X$ under $h$ is equal to the cocompact filter on $Y$. In other words, for any subset $s \subseteq X$, the image $h(s)$ has a compact complement in $Y$ if and only if $s$ has a compact complement in $X$.
Homeomorph.isDenseEmbedding theorem
(h : X ≃ₜ Y) : IsDenseEmbedding h
Full source 
theorem isDenseEmbedding (h : X ≃ₜ Y) : IsDenseEmbedding h :=
  { h.isEmbedding with dense := h.surjective.denseRange }
Homeomorphisms are Dense Embeddings
Informal description
For any homeomorphism $h \colon X \simeq_{\text{top}} Y$ between topological spaces $X$ and $Y$, the function $h$ is a dense embedding. That is, $h$ is injective, continuous, has dense image in $Y$, and induces the topology on $Y$.
Homeomorph.totallyDisconnectedSpace theorem
(h : X ≃ₜ Y) [tdc : TotallyDisconnectedSpace X] : TotallyDisconnectedSpace Y
Full source 
protected lemma totallyDisconnectedSpace (h : X ≃ₜ Y) [tdc : TotallyDisconnectedSpace X] :
    TotallyDisconnectedSpace Y :=
  (totallyDisconnectedSpace_iff Y).mpr
    (h.range_coe ▸ ((IsEmbedding.isTotallyDisconnected_range h.isEmbedding).mpr tdc))
Homeomorphism Preserves Total Disconnectedness
Informal description
Let $X$ and $Y$ be topological spaces with a homeomorphism $h \colon X \simeq_{\text{top}} Y$. If $X$ is totally disconnected, then $Y$ is also totally disconnected.
Homeomorph.map_punctured_nhds_eq theorem
(h : X ≃ₜ Y) (x : X) : map h (𝓝[≠] x) = 𝓝[≠] (h x)
Full source 
@[simp]
theorem map_punctured_nhds_eq (h : X ≃ₜ Y) (x : X) : map h (𝓝[≠] x) = 𝓝[≠] (h x) := by
  convert h.isEmbedding.map_nhdsWithin_eq ({x}{x}ᶜ) x
  rw [h.image_compl, Set.image_singleton]
Homeomorphism Preserves Punctured Neighborhood Filters
Informal description
For any homeomorphism $h \colon X \to Y$ between topological spaces $X$ and $Y$, and any point $x \in X$, the image under $h$ of the punctured neighborhood filter at $x$ (i.e., the filter of neighborhoods of $x$ excluding $x$ itself) is equal to the punctured neighborhood filter at $h(x)$ in $Y$. In symbols, $h_*(\mathcal{N}_X(x) \setminus \{x\}) = \mathcal{N}_Y(h(x)) \setminus \{h(x)\}$.
Homeomorph.comap_coclosedCompact theorem
(h : X ≃ₜ Y) : comap h (coclosedCompact Y) = coclosedCompact X
Full source 
@[simp]
theorem comap_coclosedCompact (h : X ≃ₜ Y) : comap h (coclosedCompact Y) = coclosedCompact X :=
  (hasBasis_coclosedCompact.comap h).eq_of_same_basis <| by
    simpa [comp_def] using hasBasis_coclosedCompact.comp_surjective h.injective.preimage_surjective
Homeomorphism Preserves Coclosed-Compact Filter under Preimage
Informal description
For any homeomorphism $h \colon X \to Y$ between topological spaces $X$ and $Y$, the preimage under $h$ of the coclosed-compact filter on $Y$ is equal to the coclosed-compact filter on $X$. In other words, $h^{-1}(\text{coclosedCompact}(Y)) = \text{coclosedCompact}(X)$.
Homeomorph.map_coclosedCompact theorem
(h : X ≃ₜ Y) : map h (coclosedCompact X) = coclosedCompact Y
Full source 
@[simp]
theorem map_coclosedCompact (h : X ≃ₜ Y) : map h (coclosedCompact X) = coclosedCompact Y := by
  rw [← h.comap_coclosedCompact, map_comap_of_surjective h.surjective]
Homeomorphism Preserves Coclosed-Compact Filter under Image
Informal description
For any homeomorphism $h \colon X \to Y$ between topological spaces $X$ and $Y$, the image under $h$ of the coclosed-compact filter on $X$ is equal to the coclosed-compact filter on $Y$. In other words, $h_*(\text{coclosedCompact}(X)) = \text{coclosedCompact}(Y)$.
Homeomorph.locallyConnectedSpace theorem
[i : LocallyConnectedSpace Y] (h : X ≃ₜ Y) : LocallyConnectedSpace X
Full source 
/-- If the codomain of a homeomorphism is a locally connected space, then the domain is also
a locally connected space. -/
theorem locallyConnectedSpace [i : LocallyConnectedSpace Y] (h : X ≃ₜ Y) :
    LocallyConnectedSpace X := by
  have : ∀ x, (𝓝 x).HasBasis (fun s ↦ IsOpenIsOpen s ∧ h x ∈ s ∧ IsConnected s)
      (h.symm '' ·) := fun x ↦ by
    rw [← h.symm_map_nhds_eq]
    exact (i.1 _).map _
  refine locallyConnectedSpace_of_connected_bases _ _ this fun _ _ hs ↦ ?_
  exact hs.2.2.2.image _ h.symm.continuous.continuousOn
Homeomorphism Preserves Local Connectedness of Codomain to Domain
Informal description
Let $X$ and $Y$ be topological spaces, and let $h \colon X \simeq_{\text{top}} Y$ be a homeomorphism between them. If $Y$ is a locally connected space, then $X$ is also a locally connected space.
Homeomorph.locallyCompactSpace_iff theorem
(h : X ≃ₜ Y) : LocallyCompactSpace X ↔ LocallyCompactSpace Y
Full source 
/-- The codomain of a homeomorphism is a locally compact space if and only if
the domain is a locally compact space. -/
theorem locallyCompactSpace_iff (h : X ≃ₜ Y) :
    LocallyCompactSpaceLocallyCompactSpace X ↔ LocallyCompactSpace Y := by
  exact ⟨fun _ => h.symm.isOpenEmbedding.locallyCompactSpace,
    fun _ => h.isClosedEmbedding.locallyCompactSpace⟩
Local Compactness is Preserved by Homeomorphisms
Informal description
For a homeomorphism $h \colon X \simeq_{\text{top}} Y$ between topological spaces $X$ and $Y$, the space $X$ is locally compact if and only if $Y$ is locally compact.
Homeomorph.comp_continuousOn_iff theorem
(h : X ≃ₜ Y) (f : Z → X) (s : Set Z) : ContinuousOn (h ∘ f) s ↔ ContinuousOn f s
Full source 
@[simp]
theorem comp_continuousOn_iff (h : X ≃ₜ Y) (f : Z → X) (s : Set Z) :
    ContinuousOnContinuousOn (h ∘ f) s ↔ ContinuousOn f s :=
  h.isInducing.continuousOn_iff.symm
Continuity of Composition with Homeomorphism on Subsets
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 subset $s \subseteq Z$, the composition $h \circ f$ is continuous on $s$ if and only if $f$ is continuous on $s$.
Homeomorph.comp_continuousWithinAt_iff theorem
(h : X ≃ₜ Y) (f : Z → X) (s : Set Z) (z : Z) : ContinuousWithinAt f s z ↔ ContinuousWithinAt (h ∘ f) s z
Full source 
theorem comp_continuousWithinAt_iff (h : X ≃ₜ Y) (f : Z → X) (s : Set Z) (z : Z) :
    ContinuousWithinAtContinuousWithinAt f s z ↔ ContinuousWithinAt (h ∘ f) s z :=
  h.isInducing.continuousWithinAt_iff
Characterization of Relative Continuity via Homeomorphism Composition
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. For any subset $s \subseteq Z$ and any point $z \in Z$, the function $f$ is continuous within $s$ at $z$ if and only if the composition $h \circ f$ is continuous within $s$ at $z$.
Homeomorph.subtype definition
{p : X → Prop} {q : Y → Prop} (h : X ≃ₜ Y) (h_iff : ∀ x, p x ↔ q (h x)) : { x // p x } ≃ₜ { y // q y }
Full source 
/-- 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`. -/
@[simps!]
def subtype {p : X → Prop} {q : Y → Prop} (h : X ≃ₜ Y) (h_iff : ∀ x, p x ↔ q (h x)) :
    {x // p x}{x // p x} ≃ₜ {y // q y} where
  continuous_toFun := by simpa [Equiv.coe_subtypeEquiv_eq_map] using h.continuous.subtype_map _
  continuous_invFun := by simpa [Equiv.coe_subtypeEquiv_eq_map] using
    h.symm.continuous.subtype_map _
  __ := h.subtypeEquiv h_iff
Homeomorphism between subtypes via predicate equivalence
Informal description
Given a homeomorphism $h : X \simeqₜ Y$ between topological spaces $X$ and $Y$, and predicates $p : X \to \text{Prop}$ and $q : Y \to \text{Prop}$ such that for every $x \in X$, $p(x)$ holds if and only if $q(h(x))$ holds, then the homeomorphism $h$ lifts to a homeomorphism between the subtypes $\{x \in X \mid p(x)\}$ and $\{y \in Y \mid q(y)\}$. The lifted homeomorphism is continuous in both directions, inheriting the continuity properties from $h$.
Homeomorph.subtype_toEquiv theorem
{p : X → Prop} {q : Y → Prop} (h : X ≃ₜ Y) (h_iff : ∀ x, p x ↔ q (h x)) : (h.subtype h_iff).toEquiv = h.toEquiv.subtypeEquiv h_iff
Full source 
@[simp]
lemma subtype_toEquiv {p : X → Prop} {q : Y → Prop} (h : X ≃ₜ Y) (h_iff : ∀ x, p x ↔ q (h x)) :
    (h.subtype h_iff).toEquiv = h.toEquiv.subtypeEquiv h_iff :=
  rfl
Equality of Subtype Homeomorphism and Subtype Equivalence Underlying a Homeomorphism
Informal description
Given a homeomorphism $h : X \simeqₜ Y$ between topological spaces $X$ and $Y$, and predicates $p : X \to \text{Prop}$ and $q : Y \to \text{Prop}$ such that for every $x \in X$, $p(x)$ holds if and only if $q(h(x))$ holds, the underlying equivalence of the induced homeomorphism between the subtypes $\{x \in X \mid p(x)\}$ and $\{y \in Y \mid q(y)\}$ is equal to the equivalence of subtypes induced by the underlying equivalence of $h$.
Homeomorph.sets abbrev
{s : Set X} {t : Set Y} (h : X ≃ₜ Y) (h_eq : s = h ⁻¹' t) : s ≃ₜ t
Full source 
/-- A homeomorphism `h : X ≃ₜ Y` lifts to a homeomorphism between sets `s : Set X` and `t : Set Y`
whenever `h` maps `s` onto `t`. -/
abbrev sets {s : Set X} {t : Set Y} (h : X ≃ₜ Y) (h_eq : s = h ⁻¹' t) : s ≃ₜ t :=
  h.subtype <| Set.ext_iff.mp h_eq
Homeomorphism between preimage-related subsets
Informal description
Given a homeomorphism $h : X \simeq Y$ between topological spaces $X$ and $Y$, and subsets $s \subseteq X$ and $t \subseteq Y$ such that $s = h^{-1}(t)$, then $s$ and $t$ are homeomorphic as topological subspaces.
Homeomorph.setCongr definition
{s t : Set X} (h : s = t) : s ≃ₜ t
Full source 
/-- If two sets are equal, then they are homeomorphic. -/
def setCongr {s t : Set X} (h : s = t) : s ≃ₜ t where
  continuous_toFun := continuous_inclusion h.subset
  continuous_invFun := continuous_inclusion h.symm.subset
  toEquiv := Equiv.setCongr h
Homeomorphism of equal subsets
Informal description
Given a topological space $X$ and two subsets $s, t \subseteq X$ that are equal ($s = t$), the subsets $s$ and $t$ are homeomorphic as topological spaces with the subspace topology.
Homeomorph.sumPiEquivProdPi definition
(S T : Type*) (A : S ⊕ T → Type*) [∀ st, TopologicalSpace (A st)] : (Π (st : S ⊕ T), A st) ≃ₜ (Π (s : S), A (.inl s)) × (Π (t : T), A (.inr t))
Full source 
/-- 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 sumPiEquivProdPi (S T : Type*) (A : S ⊕ T → Type*)
    [∀ st, TopologicalSpace (A st)] :
    (Π (st : S ⊕ T), A st) ≃ₜ (Π (s : S), A (.inl s)) × (Π (t : T), A (.inr t)) where
  __ := Equiv.sumPiEquivProdPi _
  continuous_toFun := .prodMk (by fun_prop) (by fun_prop)
  continuous_invFun := continuous_pi <| by rintro (s | t) <;> simp <;> fun_prop
Homeomorphism between product over a sum type and product of products
Informal description
For any types $S$ and $T$ and any family of topological spaces $A$ indexed by $S \oplus T$, the product space $\prod_{st \in S \oplus T} A(st)$ is homeomorphic to the product space $\left(\prod_{s \in S} A(\text{inl}(s))\right) \times \left(\prod_{t \in T} A(\text{inr}(t))\right)$. Here, $\text{inl}$ and $\text{inr}$ are the left and right inclusion maps into the sum type $S \oplus T$.
Homeomorph.piUnique definition
{α : Type*} [Unique α] (f : α → Type*) [∀ x, TopologicalSpace (f x)] : (Π t, f t) ≃ₜ f default
Full source 
/-- 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`.
-/
@[simps! -fullyApplied]
def piUnique {α : Type*} [Unique α] (f : α → Type*) [∀ x, TopologicalSpace (f x)] :
    (Π t, f t) ≃ₜ f default :=
  (Equiv.piUnique f).toHomeomorphOfContinuousOpen (continuous_apply default) (isOpenMap_eval _)
Homeomorphism between product over a unique type and its value at the default element
Informal description
Given a type $\alpha$ with a unique element (i.e., $[\text{Unique}\ \alpha]$) and a family of topological spaces $f : \alpha \to \text{Type*}$ indexed by $\alpha$, the product space $\prod_{t : \alpha} f\ t$ is homeomorphic to the space $f\ \text{default}$, where $\text{default}$ is the unique element of $\alpha$. This homeomorphism is constructed via the equivalence $\text{Equiv.piUnique}\ f$ and ensures continuity in both directions.
Homeomorph.piCongrLeft definition
{ι ι' : Type*} {Y : ι' → Type*} [∀ j, TopologicalSpace (Y j)] (e : ι ≃ ι') : (∀ i, Y (e i)) ≃ₜ ∀ j, Y j
Full source 
/-- `Equiv.piCongrLeft` as a homeomorphism: this is the natural homeomorphism
`Π i, Y (e i) ≃ₜ Π j, Y j` obtained from a bijection `ι ≃ ι'`. -/
@[simps! apply toEquiv]
def piCongrLeft {ι ι' : Type*} {Y : ι' → Type*} [∀ j, TopologicalSpace (Y j)]
    (e : ι ≃ ι') : (∀ i, Y (e i)) ≃ₜ ∀ j, Y j where
  continuous_toFun := continuous_pi <| e.forall_congr_right.mp fun i ↦ by
    simpa only [Equiv.toFun_as_coe, Equiv.piCongrLeft_apply_apply] using continuous_apply i
  continuous_invFun := Pi.continuous_precomp' e
  toEquiv := Equiv.piCongrLeft _ e
Homeomorphism of product spaces under index bijection
Informal description
Given an index type $\iota$, another index type $\iota'$, a family of topological spaces $\{Y_j\}_{j \in \iota'}$, and a bijection $e : \iota \simeq \iota'$, the homeomorphism $\prod_{i \in \iota} Y_{e(i)} \simeq \prod_{j \in \iota'} Y_j$ is constructed by reindexing the product via $e$. Both the forward and inverse maps are continuous, with: - The forward map being the canonical projection induced by $e$. - The inverse map being the precomposition with $e$.
Homeomorph.piCongrRight definition
{ι : Type*} {Y₁ Y₂ : ι → Type*} [∀ i, TopologicalSpace (Y₁ i)] [∀ i, TopologicalSpace (Y₂ i)] (F : ∀ i, Y₁ i ≃ₜ Y₂ i) : (∀ i, Y₁ i) ≃ₜ ∀ i, Y₂ i
Full source 
/-- `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`. -/
@[simps! apply toEquiv]
def piCongrRight {ι : Type*} {Y₁ Y₂ : ι → Type*} [∀ i, TopologicalSpace (Y₁ i)]
    [∀ i, TopologicalSpace (Y₂ i)] (F : ∀ i, Y₁ i ≃ₜ Y₂ i) : (∀ i, Y₁ i) ≃ₜ ∀ i, Y₂ i where
  continuous_toFun := Pi.continuous_postcomp' fun i ↦ (F i).continuous
  continuous_invFun := Pi.continuous_postcomp' fun i ↦ (F i).symm.continuous
  toEquiv := Equiv.piCongrRight fun i => (F i).toEquiv
Component-wise homeomorphism of product spaces
Informal description
Given an index type $\iota$ and two families of topological spaces $\{Y_1 i\}_{i \in \iota}$ and $\{Y_2 i\}_{i \in \iota}$, along with a family of homeomorphisms $F : \forall i, Y_1 i \simeq Y_2 i$, the homeomorphism $\prod_{i} Y_1 i \simeq \prod_{i} Y_2 i$ is constructed by applying each $F i$ component-wise to the product space. This homeomorphism is continuous in both directions, with the forward map obtained by post-composing with each $F i$ and the inverse map obtained by post-composing with each $(F i)^{-1}$.
Homeomorph.piCongrRight_symm theorem
{ι : Type*} {Y₁ Y₂ : ι → Type*} [∀ i, TopologicalSpace (Y₁ i)] [∀ i, TopologicalSpace (Y₂ i)] (F : ∀ i, Y₁ i ≃ₜ Y₂ i) : (piCongrRight F).symm = piCongrRight fun i => (F i).symm
Full source 
@[simp]
theorem piCongrRight_symm {ι : Type*} {Y₁ Y₂ : ι → Type*} [∀ i, TopologicalSpace (Y₁ i)]
    [∀ i, TopologicalSpace (Y₂ i)] (F : ∀ i, Y₁ i ≃ₜ Y₂ i) :
    (piCongrRight F).symm = piCongrRight fun i => (F i).symm :=
  rfl
Inverse of Component-wise Homeomorphism Equals Component-wise Inverses
Informal description
Given an index type $\iota$ and two families of topological spaces $\{Y_1 i\}_{i \in \iota}$ and $\{Y_2 i\}_{i \in \iota}$, along with a family of homeomorphisms $F : \forall i, Y_1 i \simeq Y_2 i$, the inverse of the component-wise homeomorphism $\prod_{i} Y_1 i \simeq \prod_{i} Y_2 i$ is equal to the component-wise homeomorphism obtained by taking the inverse of each $F i$.
Homeomorph.piCongr definition
{ι₁ ι₂ : Type*} {Y₁ : ι₁ → Type*} {Y₂ : ι₂ → Type*} [∀ i₁, TopologicalSpace (Y₁ i₁)] [∀ i₂, TopologicalSpace (Y₂ i₂)] (e : ι₁ ≃ ι₂) (F : ∀ i₁, Y₁ i₁ ≃ₜ Y₂ (e i₁)) : (∀ i₁, Y₁ i₁) ≃ₜ ∀ i₂, Y₂ i₂
Full source 
/-- `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₁ : ι₁`. -/
@[simps! apply toEquiv]
def piCongr {ι₁ ι₂ : Type*} {Y₁ : ι₁ → Type*} {Y₂ : ι₂ → Type*}
    [∀ i₁, TopologicalSpace (Y₁ i₁)] [∀ i₂, TopologicalSpace (Y₂ i₂)]
    (e : ι₁ ≃ ι₂) (F : ∀ i₁, Y₁ i₁ ≃ₜ Y₂ (e i₁)) : (∀ i₁, Y₁ i₁) ≃ₜ ∀ i₂, Y₂ i₂ :=
  (Homeomorph.piCongrRight F).trans (Homeomorph.piCongrLeft e)
Homeomorphism of product spaces under index bijection and component-wise homeomorphisms
Informal description
Given two index types $\iota_1$ and $\iota_2$, two families of topological spaces $\{Y_1 i_1\}_{i_1 \in \iota_1}$ and $\{Y_2 i_2\}_{i_2 \in \iota_2}$, a bijection $e : \iota_1 \simeq \iota_2$, and a family of homeomorphisms $F : \forall i_1, Y_1 i_1 \simeq Y_2 (e i_1)$, the homeomorphism $\prod_{i_1} Y_1 i_1 \simeq \prod_{i_2} Y_2 i_2$ is constructed by first applying the component-wise homeomorphism $F$ and then reindexing via $e$. This homeomorphism is continuous in both directions, with the forward map obtained by post-composing with each $F i_1$ and then reindexing, and the inverse map obtained by reindexing and then post-composing with each $(F i_1)^{-1}$.
Homeomorph.ulift definition
{X : Type v} [TopologicalSpace X] : ULift.{u, v} X ≃ₜ X
Full source 
/-- `ULift X` is homeomorphic to `X`. -/
def ulift.{u, v} {X : Type v} [TopologicalSpace X] : ULiftULift.{u, v} X ≃ₜ X where
  continuous_toFun := continuous_uliftDown
  continuous_invFun := continuous_uliftUp
  toEquiv := Equiv.ulift
Homeomorphism between `ULift X` and `X`
Informal description
The homeomorphism between the lifted type `ULift X` and the topological space `X`, where the forward map is the continuous projection `ULift.down` and the inverse map is the continuous lifting `ULift.up`. This establishes that `ULift X` and `X` are topologically equivalent.
Homeomorph.sumArrowHomeomorphProdArrow definition
{ι ι' : Type*} : (ι ⊕ ι' → X) ≃ₜ (ι → X) × (ι' → X)
Full source 
/-- The natural homeomorphism `(ι ⊕ ι' → X) ≃ₜ (ι → X) × (ι' → X)`.
`Equiv.sumArrowEquivProdArrow` as a homeomorphism. -/
@[simps!]
def sumArrowHomeomorphProdArrow {ι ι' : Type*} : (ι ⊕ ι' → X) ≃ₜ (ι → X) × (ι' → X)  where
  toEquiv := Equiv.sumArrowEquivProdArrow _ _ _
  continuous_toFun := by
    dsimp [Equiv.sumArrowEquivProdArrow]
    fun_prop
  continuous_invFun := continuous_pi fun i ↦ match i with
    | .inl i => by apply (continuous_apply _).comp' continuous_fst
    | .inr i => by apply (continuous_apply _).comp' continuous_snd
Homeomorphism between function spaces on sum and product types
Informal description
The natural homeomorphism between the space of functions from the sum type $\iota \oplus \iota'$ to $X$ and the product space $(\iota \to X) \times (\iota' \to X)$. This is the topological version of the equivalence `Equiv.sumArrowEquivProdArrow`, where both the forward and inverse maps are continuous.
Fin.continuous_append theorem
(m n : ℕ) : Continuous fun (p : (Fin m → X) × (Fin n → X)) ↦ Fin.append p.1 p.2
Full source 
theorem _root_.Fin.continuous_append (m n : ℕ) :
    Continuous fun (p : (Fin m → X) × (Fin n → X)) ↦ Fin.append p.1 p.2 := by
  suffices Continuous (Fin.appendEquiv m n) by exact this
  rw [Fin.appendEquiv_eq_Homeomorph]
  exact Homeomorph.continuous_toFun _
Continuity of Finite Tuple Concatenation
Informal description
For any natural numbers $m$ and $n$, the concatenation function $\text{Fin.append} \colon (\text{Fin}\, m \to X) \times (\text{Fin}\, n \to X) \to \text{Fin}\, (m + n) \to X$ is continuous, where the domain is equipped with the product topology and the codomain with the product topology (i.e., the topology of pointwise convergence).
Fin.appendHomeomorph definition
(m n : ℕ) : (Fin m → X) × (Fin n → X) ≃ₜ (Fin (m + n) → X)
Full source 
/-- The natural homeomorphism between `(Fin m → X) × (Fin n → X)` and `Fin (m + n) → X`.
`Fin.appendEquiv` as a homeomorphism -/
@[simps!]
def _root_.Fin.appendHomeomorph (m n : ℕ) : (Fin m → X) × (Fin n → X)(Fin m → X) × (Fin n → X) ≃ₜ (Fin (m + n) → X) where
  toEquiv := Fin.appendEquiv m n
  continuous_toFun := Fin.continuous_append m n
  continuous_invFun := by
    rw [Fin.appendEquiv_eq_Homeomorph]
    exact Homeomorph.continuous_invFun _
Homeomorphism for concatenated finite function spaces
Informal description
The natural homeomorphism between the product space $( \text{Fin}\, m \to X ) \times ( \text{Fin}\, n \to X )$ and the function space $\text{Fin}\, (m + n) \to X$, where both spaces are equipped with the product topology. Given a pair of functions $(f, g)$ where $f : \text{Fin}\, m \to X$ and $g : \text{Fin}\, n \to X$, the forward map constructs their concatenation $h : \text{Fin}\, (m + n) \to X$ such that for $i < m$, $h\, i = f\, i$, and for $m \leq i < m + n$, $h\, i = g\, (i - m)$. The inverse map splits a function $h : \text{Fin}\, (m + n) \to X$ into two functions $f : \text{Fin}\, m \to X$ and $g : \text{Fin}\, n \to X$ by restricting $h$ to the appropriate subdomains. Both the forward and inverse maps are continuous.
Fin.appendHomeomorph_toEquiv theorem
(m n : ℕ) : (Fin.appendHomeomorph (X := X) m n).toEquiv = Fin.appendEquiv m n
Full source 
@[simp]
theorem _root_.Fin.appendHomeomorph_toEquiv (m n : ℕ) :
    (Fin.appendHomeomorph (X := X) m n).toEquiv = Fin.appendEquiv m n :=
  rfl
Equivalence Underlying the Finite Concatenation Homeomorphism
Informal description
For any natural numbers $m$ and $n$, the underlying equivalence of the homeomorphism `Fin.appendHomeomorph` between the product space $( \text{Fin}\, m \to X ) \times ( \text{Fin}\, n \to X )$ and the function space $\text{Fin}\, (m + n) \to X$ is equal to the equivalence `Fin.appendEquiv m n$.
Homeomorph.sigmaProdDistrib definition
: (Σ i, X i) × Y ≃ₜ Σ i, X i × Y
Full source 
/-- `(Σ i, X i) × Y` is homeomorphic to `Σ i, (X i × Y)`. -/
@[simps! apply symm_apply toEquiv]
def sigmaProdDistrib : (Σ i, X i) × Y(Σ i, X i) × Y ≃ₜ Σ i, X i × Y :=
  Homeomorph.symm <|
    (Equiv.sigmaProdDistrib X Y).symm.toHomeomorphOfContinuousOpen
      (continuous_sigma fun _ => continuous_sigmaMk.fst'.prodMk continuous_snd)
      (isOpenMap_sigma.2 fun _ => isOpenMap_sigmaMk.prodMap IsOpenMap.id)
Distributivity of product over indexed sum in topological spaces
Informal description
The product $(\Sigma i, X_i) \times Y$ is homeomorphic to the disjoint union $\Sigma i, (X_i \times Y)$, where $\{X_i\}_{i \in \iota}$ is a family of topological spaces indexed by $\iota$ and $Y$ is another topological space. More precisely, the homeomorphism maps a pair $((i, x), y)$ to $(i, (x, y))$ and vice versa, establishing a continuous bijection with continuous inverse between these two spaces.
Homeomorph.funUnique definition
(ι X : Type*) [Unique ι] [TopologicalSpace X] : (ι → X) ≃ₜ X
Full source 
/-- If `ι` has a unique element, then `ι → X` is homeomorphic to `X`. -/
@[simps! -fullyApplied]
def funUnique (ι X : Type*) [Unique ι] [TopologicalSpace X] : (ι → X) ≃ₜ X where
  toEquiv := Equiv.funUnique ι X
  continuous_toFun := continuous_apply _
  continuous_invFun := continuous_pi fun _ => continuous_id
Homeomorphism between functions from a singleton type and their codomain
Informal description
Given a topological space $X$ and a type $\iota$ with a unique element, the space of functions from $\iota$ to $X$ is homeomorphic to $X$ itself. The homeomorphism maps a function $f \colon \iota \to X$ to its value at the unique element of $\iota$, and conversely, any element $x \in X$ can be viewed as the constant function sending the unique element of $\iota$ to $x$. Both the forward and inverse maps are continuous with respect to the product topology on $\iota \to X$ and the original topology on $X$.
Homeomorph.piFinTwo definition
(X : Fin 2 → Type u) [∀ i, TopologicalSpace (X i)] : (∀ i, X i) ≃ₜ X 0 × X 1
Full source 
/-- Homeomorphism between dependent functions `Π i : Fin 2, X i` and `X 0 × X 1`. -/
@[simps! -fullyApplied]
def piFinTwo.{u} (X : Fin 2 → Type u) [∀ i, TopologicalSpace (X i)] : (∀ i, X i) ≃ₜ X 0 × X 1 where
  toEquiv := piFinTwoEquiv X
  continuous_toFun := (continuous_apply 0).prodMk (continuous_apply 1)
  continuous_invFun := continuous_pi <| Fin.forall_fin_two.2 ⟨continuous_fst, continuous_snd⟩
Homeomorphism between dependent functions on `Fin 2` and pairs
Informal description
The homeomorphism between the space of dependent functions `Π i : Fin 2, X i` and the product space `X 0 × X 1`, where each `X i` is a topological space. This homeomorphism is constructed by: - The forward direction maps a function `f` to the pair `(f 0, f 1)`. - The backward direction maps a pair `(x, y)` to the function that takes `0` to `x` and `1` to `y`. Both directions are continuous with respect to the product topology on `X 0 × X 1` and the topology of pointwise convergence on `Π i : Fin 2, X i`.
Homeomorph.finTwoArrow definition
: (Fin 2 → X) ≃ₜ X × X
Full source 
/-- Homeomorphism between `X² = Fin 2 → X` and `X × X`. -/
@[simps! -fullyApplied]
def finTwoArrow : (Fin 2 → X) ≃ₜ X × X :=
  { piFinTwo fun _ => X with toEquiv := finTwoArrowEquiv X }
Homeomorphism between functions on `Fin 2` and pairs in $X \times X$
Informal description
The homeomorphism between the space of functions from `Fin 2` to a topological space $X$ and the product space $X \times X$. Specifically: - The forward direction maps a function $f : \text{Fin } 2 \to X$ to the pair $(f(0), f(1))$. - The backward direction maps a pair $(x, y) \in X \times X$ to the function that takes $0$ to $x$ and $1$ to $y$. Both directions are continuous with respect to the product topology on $X \times X$ and the topology of pointwise convergence on $\text{Fin } 2 \to X$.
Homeomorph.image definition
(e : X ≃ₜ Y) (s : Set X) : s ≃ₜ e '' s
Full source 
/-- A subset of a topological space is homeomorphic to its image under a homeomorphism.
-/
@[simps!]
def image (e : X ≃ₜ Y) (s : Set X) : s ≃ₜ e '' s where
  -- TODO: by continuity!
  continuous_toFun := e.continuous.continuousOn.restrict_mapsTo (mapsTo_image _ _)
  continuous_invFun := (e.symm.continuous.comp continuous_subtype_val).codRestrict _
  toEquiv := e.toEquiv.image s
Homeomorphism between a subset and its image under a homeomorphism
Informal description
Given a homeomorphism $e : X \simeqₜ Y$ between topological spaces $X$ and $Y$, and a subset $s \subseteq X$, the subset $s$ is homeomorphic to its image $e(s) \subseteq Y$ under $e$. The homeomorphism is constructed by restricting $e$ to $s$ and its inverse to $e(s)$, both of which are continuous.
Homeomorph.Set.univ definition
(X : Type*) [TopologicalSpace X] : (univ : Set X) ≃ₜ X
Full source 
/-- `Set.univ X` is homeomorphic to `X`. -/
@[simps! -fullyApplied]
def Set.univ (X : Type*) [TopologicalSpace X] : (univ : Set X) ≃ₜ X where
  toEquiv := Equiv.Set.univ X
  continuous_toFun := continuous_subtype_val
  continuous_invFun := continuous_id.subtype_mk _
Homeomorphism between universal set and base space
Informal description
The universal set of a topological space $X$ is homeomorphic to $X$ itself. The homeomorphism is given by the natural bijection between the set of all elements of $X$ and $X$, where: - The forward map is the inclusion of the universal set into $X$ (which is continuous as it's the restriction of the identity map). - The inverse map sends each element $x \in X$ to itself considered as an element of the universal set (which is also continuous).
Homeomorph.Set.prod definition
(s : Set X) (t : Set Y) : ↥(s ×ˢ t) ≃ₜ s × t
Full source 
/-- `s ×ˢ t` is homeomorphic to `s × t`. -/
@[simps!]
def Set.prod (s : Set X) (t : Set Y) : ↥(s ×ˢ t) ≃ₜ s × t where
  toEquiv := Equiv.Set.prod s t
  continuous_toFun :=
    (continuous_subtype_val.fst.subtype_mk _).prodMk (continuous_subtype_val.snd.subtype_mk _)
  continuous_invFun :=
    (continuous_subtype_val.fst'.prodMk continuous_subtype_val.snd').subtype_mk _
Homeomorphism between product set and product space of subsets
Informal description
For any topological spaces $X$ and $Y$, and subsets $s \subseteq X$ and $t \subseteq Y$, the product set $s \timesˢ t$ is homeomorphic to the product topological space $s \times t$. Here, $s \timesˢ t$ denotes the Cartesian product of sets, and $s \times t$ denotes the product space with the subspace topology inherited from $X \times Y$.
Homeomorph.piEquivPiSubtypeProd definition
(p : ι → Prop) (Y : ι → Type*) [∀ i, TopologicalSpace (Y i)] [DecidablePred p] : (∀ i, Y i) ≃ₜ (∀ i : { x // p x }, Y i) × ∀ i : { x // ¬p x }, Y i
Full source 
/-- 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. -/
@[simps!]
def piEquivPiSubtypeProd (p : ι → Prop) (Y : ι → Type*) [∀ i, TopologicalSpace (Y i)]
    [DecidablePred p] : (∀ i, Y i) ≃ₜ (∀ i : { x // p x }, Y i) × ∀ i : { x // ¬p x }, Y i where
  toEquiv := Equiv.piEquivPiSubtypeProd p Y
  continuous_toFun := by
    apply Continuous.prodMk <;> exact continuous_pi fun j => continuous_apply j.1
  continuous_invFun :=
    continuous_pi fun j => by
      dsimp only [Equiv.piEquivPiSubtypeProd]; split_ifs
      exacts [(continuous_apply _).comp continuous_fst, (continuous_apply _).comp continuous_snd]
Homeomorphism between dependent function space and product of restricted function spaces
Informal description
Given a type $\iota$, a decidable predicate $p : \iota \to \text{Prop}$, and a family of topological spaces $(Y_i)_{i \in \iota}$, the space of dependent functions $\prod_{i \in \iota} Y_i$ is homeomorphic to the product space $\prod_{i \in \{x \mid p x\}} Y_i \times \prod_{i \in \{x \mid \neg p x\}} Y_i$. The homeomorphism maps a function $f$ to the pair $(f \restriction_{\{x \mid p x\}}, f \restriction_{\{x \mid \neg p x\}})$, and its inverse reconstructs $f$ by case analysis on $p x$. Both the homeomorphism and its inverse are continuous with respect to the product topologies.
Homeomorph.piSplitAt definition
(Y : ι → Type*) [∀ j, TopologicalSpace (Y j)] : (∀ j, Y j) ≃ₜ Y i × ∀ j : { j // j ≠ i }, Y j
Full source 
/-- 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. -/
@[simps!]
def piSplitAt (Y : ι → Type*) [∀ j, TopologicalSpace (Y j)] :
    (∀ j, Y j) ≃ₜ Y i × ∀ j : { j // j ≠ i }, Y j where
  toEquiv := Equiv.piSplitAt i Y
  continuous_toFun := (continuous_apply i).prodMk (continuous_pi fun j => continuous_apply j.1)
  continuous_invFun :=
    continuous_pi fun j => by
      dsimp only [Equiv.piSplitAt]
      split_ifs with h
      · subst h
        exact continuous_fst
      · exact (continuous_apply _).comp continuous_snd
Homeomorphism for splitting dependent function space at a point
Informal description
For a family of topological spaces $\{Y_j\}_{j \in \iota}$ indexed by a type $\iota$ with decidable equality, and a fixed index $i \in \iota$, the space of dependent functions $\prod_{j \in \iota} Y_j$ is homeomorphic to the product space $Y_i \times \prod_{j \in \{j' \mid j' \neq i\}} Y_j$. The homeomorphism maps a function $f$ to the pair $(f(i), f \restriction_{\{j \mid j \neq i\}})$, and its inverse reconstructs $f$ by evaluating at $i$ or using the restriction as appropriate. Both the homeomorphism and its inverse are continuous with respect to the product topologies.
Homeomorph.funSplitAt definition
: (ι → Y) ≃ₜ Y × ({ j // j ≠ i } → Y)
Full source 
/-- 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. -/
@[simps!]
def funSplitAt : (ι → Y) ≃ₜ Y × ({ j // j ≠ i } → Y) :=
  piSplitAt i _
Homeomorphism for splitting function space at a point
Informal description
For a topological space $Y$ and a type $\iota$ with decidable equality, the space of functions $\iota \to Y$ is homeomorphic to the product space $Y \times (\{j \mid j \neq i\} \to Y)$ for any fixed index $i \in \iota$. The homeomorphism maps a function $f$ to the pair $(f(i), f \restriction_{\{j \mid j \neq i\}})$, and its inverse reconstructs $f$ by evaluating at $i$ or using the restriction as appropriate. Both the homeomorphism and its inverse are continuous with respect to the product topologies.
Continuous.continuous_symm_of_equiv_compact_to_t2 theorem
[CompactSpace X] [T2Space Y] {f : X ≃ Y} (hf : Continuous f) : Continuous f.symm
Full source 
theorem continuous_symm_of_equiv_compact_to_t2 [CompactSpace X] [T2Space Y] {f : X ≃ Y}
    (hf : Continuous f) : Continuous f.symm := by
  rw [continuous_iff_isClosed]
  intro C hC
  have hC' : IsClosed (f '' C) := (hC.isCompact.image hf).isClosed
  rwa [Equiv.image_eq_preimage] at hC'
Inverse of a Continuous Bijection from Compact to Hausdorff is Continuous
Informal description
Let $X$ be a compact topological space and $Y$ a Hausdorff space. Given a bijection $f \colon X \to Y$ such that $f$ is continuous, the inverse function $f^{-1} \colon Y \to X$ is also continuous.
Continuous.homeoOfEquivCompactToT2 definition
[CompactSpace X] [T2Space Y] {f : X ≃ Y} (hf : Continuous f) : X ≃ₜ Y
Full source 
/-- 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`). -/
@[simps toEquiv]
def homeoOfEquivCompactToT2 [CompactSpace X] [T2Space Y] {f : X ≃ Y} (hf : Continuous f) : X ≃ₜ Y :=
  { f with
    continuous_toFun := hf
    continuous_invFun := hf.continuous_symm_of_equiv_compact_to_t2 }
Homeomorphism from continuous bijection between compact and Hausdorff spaces
Informal description
Given a compact topological space $X$ and a Hausdorff space $Y$, any continuous bijection $f \colon X \to Y$ induces a homeomorphism between $X$ and $Y$. The homeomorphism has $f$ as its forward map and the continuous inverse of $f$ as its backward map.
IsHomeomorph.homeomorph definition
: X ≃ₜ Y
Full source 
/-- Bundled homeomorphism constructed from a map that is a homeomorphism. -/
@[simps! toEquiv apply symm_apply]
noncomputable def homeomorph : X ≃ₜ Y where
  continuous_toFun := hf.1
  continuous_invFun := by
    rw [continuous_iff_continuousOn_univ, ← hf.bijective.2.range_eq]
    exact hf.isOpenMap.continuousOn_range_of_leftInverse (leftInverse_surjInv hf.bijective)
  toEquiv := Equiv.ofBijective f hf.bijective
Homeomorphism from a bijective open continuous map
Informal description
Given a bijective continuous function \( f : X \to Y \) between topological spaces where \( f \) is also an open map, the homeomorphism \( X \simeq Y \) is constructed with \( f \) as the forward map and its inverse \( f^{-1} \) as the backward map, both of which are continuous.
IsHomeomorph.isClosedMap theorem
: IsClosedMap f
Full source 
protected lemma isClosedMap : IsClosedMap f := (hf.homeomorph f).isClosedMap
Homeomorphisms are closed maps
Informal description
If $f \colon X \to Y$ is a homeomorphism between topological spaces, then $f$ is a closed map. That is, for every closed subset $U \subseteq X$, the image $f(U)$ is closed in $Y$.
IsHomeomorph.isInducing theorem
: IsInducing f
Full source 
lemma isInducing : IsInducing f := (hf.homeomorph f).isInducing
Homeomorphisms are Inducing Maps
Informal description
If $f \colon X \to Y$ is a homeomorphism between topological spaces, then $f$ is an inducing map. That is, the topology on $X$ is the same as the topology induced by $f$ from $Y$.
IsHomeomorph.isQuotientMap theorem
: IsQuotientMap f
Full source 
lemma isQuotientMap : IsQuotientMap f := (hf.homeomorph f).isQuotientMap
Homeomorphisms are quotient maps
Informal description
If a function $f \colon X \to Y$ between topological spaces is a homeomorphism, then it is a quotient map. That is, $f$ is surjective and a subset $U \subseteq Y$ is open if and only if its preimage $f^{-1}(U)$ is open in $X$.
IsHomeomorph.isEmbedding theorem
: IsEmbedding f
Full source 
lemma isEmbedding : IsEmbedding f := (hf.homeomorph f).isEmbedding
Homeomorphisms are Topological Embeddings
Informal description
If $f \colon X \to Y$ is a homeomorphism between topological spaces, then $f$ is a topological embedding. That is, $f$ is injective and the topology on $X$ is the coarsest topology that makes $f$ continuous.
IsHomeomorph.isOpenEmbedding theorem
: IsOpenEmbedding f
Full source 
lemma isOpenEmbedding : IsOpenEmbedding f := (hf.homeomorph f).isOpenEmbedding
Homeomorphisms are Open Embeddings
Informal description
If a function $f \colon X \to Y$ between topological spaces is a homeomorphism, then it is an open embedding. That is, $f$ is injective, continuous, and maps open subsets of $X$ to open subsets of $Y$, while also inducing the topology on $X$ from $Y$.
IsHomeomorph.isClosedEmbedding theorem
: IsClosedEmbedding f
Full source 
lemma isClosedEmbedding : IsClosedEmbedding f := (hf.homeomorph f).isClosedEmbedding
Homeomorphisms are Closed Embeddings
Informal description
If a function $f \colon X \to Y$ between topological spaces is a homeomorphism, then it is a closed embedding. That is, $f$ is injective, continuous, maps closed subsets of $X$ to closed subsets of $Y$, and induces the topology on $X$ from $Y$.
IsHomeomorph.isDenseEmbedding theorem
: IsDenseEmbedding f
Full source 
lemma isDenseEmbedding : IsDenseEmbedding f := (hf.homeomorph f).isDenseEmbedding
Homeomorphisms are dense embeddings
Informal description
If a continuous bijection $f \colon X \to Y$ between topological spaces is a homeomorphism (i.e., its inverse is also continuous), then $f$ is a dense embedding. This means: 1. $f$ is injective, 2. $f$ is continuous, 3. the image of $f$ is dense in $Y$, and 4. $f$ induces the topology on $Y$.
isHomeomorph_iff_exists_homeomorph theorem
: IsHomeomorph f ↔ ∃ h : X ≃ₜ Y, h = f
Full source 
/-- A map is a homeomorphism iff it is the map underlying a bundled homeomorphism `h : X ≃ₜ Y`. -/
lemma isHomeomorph_iff_exists_homeomorph : IsHomeomorphIsHomeomorph f ↔ ∃ h : X ≃ₜ Y, h = f :=
  ⟨fun hf => ⟨hf.homeomorph f, rfl⟩, fun ⟨h, h'⟩ => h' ▸ h.isHomeomorph⟩
Characterization of Homeomorphisms via Bundled Equivalences
Informal description
A continuous function $f \colon X \to Y$ between topological spaces is a homeomorphism if and only if there exists a bundled homeomorphism $h \colon X \simeq_{\text{top}} Y$ such that $h = f$.
isHomeomorph_iff_exists_inverse theorem
: IsHomeomorph f ↔ Continuous f ∧ ∃ g : Y → X, LeftInverse g f ∧ RightInverse g f ∧ Continuous g
Full source 
/-- A map is a homeomorphism iff it is continuous and has a continuous inverse. -/
lemma isHomeomorph_iff_exists_inverse : IsHomeomorphIsHomeomorph f ↔ Continuous f ∧ ∃ g : Y → X,
    LeftInverse g f ∧ RightInverse g f ∧ Continuous g := by
  refine ⟨fun hf ↦ ⟨hf.continuous, ?_⟩, fun ⟨hf, g, hg⟩ ↦ ?_⟩
  · let h := hf.homeomorph f
    exact ⟨h.symm, h.left_inv, h.right_inv, h.continuous_invFun⟩
  · exact (Homeomorph.mk ⟨f, g, hg.1, hg.2.1⟩ hf hg.2.2).isHomeomorph
Characterization of Homeomorphisms via Continuous Inverse
Informal description
A function $f \colon X \to Y$ between topological spaces is a homeomorphism if and only if it is continuous and there exists a continuous function $g \colon Y \to X$ such that $g$ is both a left and right inverse of $f$.
isHomeomorph_iff_isEmbedding_surjective theorem
: IsHomeomorph f ↔ IsEmbedding f ∧ Surjective f
Full source 
/-- A map is a homeomorphism iff it is a surjective embedding. -/
lemma isHomeomorph_iff_isEmbedding_surjective : IsHomeomorphIsHomeomorph f ↔ IsEmbedding f ∧ Surjective f where
  mp hf := ⟨hf.isEmbedding, hf.surjective⟩
  mpr h := ⟨h.1.continuous, ((isOpenEmbedding_iff f).2 ⟨h.1, h.2.range_eq ▸ isOpen_univ⟩).isOpenMap,
    h.1.injective, h.2⟩
Characterization of Homeomorphisms as Surjective Embeddings
Informal description
A continuous function $f \colon X \to Y$ between topological spaces is a homeomorphism if and only if it is a topological embedding and surjective.
isHomeomorph_iff_continuous_isClosedMap_bijective theorem
: IsHomeomorph f ↔ Continuous f ∧ IsClosedMap f ∧ Function.Bijective f
Full source 
/-- A map is a homeomorphism iff it is continuous, closed and bijective. -/
lemma isHomeomorph_iff_continuous_isClosedMap_bijective  : IsHomeomorphIsHomeomorph f ↔
    Continuous f ∧ IsClosedMap f ∧ Function.Bijective f :=
  ⟨fun hf => ⟨hf.continuous, hf.isClosedMap, hf.bijective⟩, fun ⟨hf, hf', hf''⟩ =>
    ⟨hf, fun _ hu => isClosed_compl_iff.1 (image_compl_eq hf'' ▸ hf' _ hu.isClosed_compl), hf''⟩⟩
Characterization of Homeomorphisms via Continuity, Closedness, and Bijectivity
Informal description
A function $f \colon X \to Y$ between topological spaces is a homeomorphism if and only if it is continuous, a closed map, and bijective.
isHomeomorph_iff_continuous_bijective theorem
[CompactSpace X] [T2Space Y] : IsHomeomorph f ↔ Continuous f ∧ Bijective f
Full source 
/-- A map from a compact space to a T2 space is a homeomorphism iff it is continuous and
  bijective. -/
lemma isHomeomorph_iff_continuous_bijective [CompactSpace X] [T2Space Y] :
    IsHomeomorphIsHomeomorph f ↔ Continuous f ∧ Bijective f := by
  rw [isHomeomorph_iff_continuous_isClosedMap_bijective]
  refine and_congr_right fun hf ↦ ?_
  rw [eq_true hf.isClosedMap, true_and]
Characterization of Homeomorphisms between Compact and Hausdorff Spaces via Continuity and Bijectivity
Informal description
Let $X$ be a compact topological space and $Y$ a Hausdorff space. A function $f \colon X \to Y$ is a homeomorphism if and only if it is continuous and bijective.
IsHomeomorph.sumMap theorem
{g : Z → W} (hf : IsHomeomorph f) (hg : IsHomeomorph g) : IsHomeomorph (Sum.map f g)
Full source 
lemma IsHomeomorph.sumMap {g : Z → W} (hf : IsHomeomorph f) (hg : IsHomeomorph g) :
    IsHomeomorph (Sum.map f g) := ⟨hf.1.sumMap hg.1, hf.2.sumMap hg.2, hf.3.sumMap hg.3⟩
Homeomorphism of Sum Spaces via Sum Map
Informal description
Let $f : X \to Y$ and $g : Z \to W$ be homeomorphisms between topological spaces. Then the sum map $f \oplus g : X \oplus Z \to Y \oplus W$, defined by $(f \oplus g)(\text{inl}(x)) = \text{inl}(f(x))$ and $(f \oplus g)(\text{inr}(z)) = \text{inr}(g(z))$, is also a homeomorphism.
IsHomeomorph.prodMap theorem
{g : Z → W} (hf : IsHomeomorph f) (hg : IsHomeomorph g) : IsHomeomorph (Prod.map f g)
Full source 
lemma IsHomeomorph.prodMap {g : Z → W} (hf : IsHomeomorph f) (hg : IsHomeomorph g) :
    IsHomeomorph (Prod.map f g) := ⟨hf.1.prodMap hg.1, hf.2.prodMap hg.2, hf.3.prodMap hg.3⟩
Homeomorphism of Product Spaces via Component Homeomorphisms
Informal description
Let $f : X \to Y$ and $g : Z \to W$ be homeomorphisms between topological spaces. Then the product map $f \times g : X \times Z \to Y \times W$ defined by $(f \times g)(x, z) = (f(x), g(z))$ is also a homeomorphism.
IsHomeomorph.sigmaMap theorem
{ι κ : Type*} {X : ι → Type*} {Y : κ → Type*} [∀ i, TopologicalSpace (X i)] [∀ i, TopologicalSpace (Y i)] {f : ι → κ} (hf : Bijective f) {g : (i : ι) → X i → Y (f i)} (hg : ∀ i, IsHomeomorph (g i)) : IsHomeomorph (Sigma.map f g)
Full source 
lemma IsHomeomorph.sigmaMap {ι κ : Type*} {X : ι → Type*} {Y : κ → Type*}
    [∀ i, TopologicalSpace (X i)] [∀ i, TopologicalSpace (Y i)] {f : ι → κ}
    (hf : Bijective f) {g : (i : ι) → X i → Y (f i)} (hg : ∀ i, IsHomeomorph (g i)) :
    IsHomeomorph (Sigma.map f g) := by
  simp_rw [isHomeomorph_iff_isEmbedding_surjective,] at hg ⊢
  exact ⟨(isEmbedding_sigmaMap hf.1).2 fun i ↦ (hg i).1, hf.2.sigma_map fun i ↦ (hg i).2⟩
Homeomorphism of Sigma Types via Bijective Index Mapping and Component Homeomorphisms
Informal description
Let $\{X_i\}_{i \in \iota}$ and $\{Y_j\}_{j \in \kappa}$ be families of topological spaces indexed by types $\iota$ and $\kappa$ respectively. Given a bijective function $f \colon \iota \to \kappa$ and a family of homeomorphisms $g_i \colon X_i \to Y_{f(i)}$ for each $i \in \iota$, the induced map $\Sigma f g \colon \Sigma X \to \Sigma Y$ defined by $(\Sigma f g)(i, x) = (f(i), g_i(x))$ is a homeomorphism.
IsHomeomorph.pi_map theorem
{ι : Type*} {X Y : ι → Type*} [∀ 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))
Full source 
lemma IsHomeomorph.pi_map {ι : Type*} {X Y : ι → Type*} [∀ 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)) :=
  (Homeomorph.piCongrRight fun i ↦ (h i).homeomorph (f i)).isHomeomorph
Component-wise Homeomorphism of Product Spaces
Informal description
Let $\{X_i\}_{i \in \iota}$ and $\{Y_i\}_{i \in \iota}$ be families of topological spaces indexed by a type $\iota$, and for each $i \in \iota$, let $f_i \colon X_i \to Y_i$ be a homeomorphism. Then the component-wise map $f \colon \prod_{i \in \iota} X_i \to \prod_{i \in \iota} Y_i$ defined by $f(x)(i) = f_i(x(i))$ is also a homeomorphism.