doc-next-gen

Mathlib.Topology.Connected.TotallyDisconnected

Module docstring

{"# Totally disconnected and totally separated topological spaces

Main definitions

We define the following properties for sets in a topological space:

  • IsTotallyDisconnected: all of its connected components are singletons.
  • IsTotallySeparated: any two points can be separated by two disjoint opens that cover the set.

For both of these definitions, we also have a class stating that the whole space satisfies that property: TotallyDisconnectedSpace, TotallySeparatedSpace. "}

IsTotallyDisconnected definition
(s : Set α) : Prop
Full source 
/-- A set `s` is called totally disconnected if every subset `t ⊆ s` which is preconnected is
a subsingleton, ie either empty or a singleton. -/
def IsTotallyDisconnected (s : Set α) : Prop :=
  ∀ t, t ⊆ s → IsPreconnected t → t.Subsingleton
Totally disconnected subset of a topological space
Informal description
A subset $s$ of a topological space $\alpha$ is called *totally disconnected* if every nonempty preconnected subset $t \subseteq s$ is a singleton. In other words, the only connected components of $s$ are single points.
isTotallyDisconnected_empty theorem
: IsTotallyDisconnected (∅ : Set α)
Full source 
theorem isTotallyDisconnected_empty : IsTotallyDisconnected (∅ : Set α) := fun _ ht _ _ x_in _ _ =>
  (ht x_in).elim
Empty Set is Totally Disconnected
Informal description
The empty set is totally disconnected in any topological space $\alpha$.
TotallyDisconnectedSpace structure
(α : Type u) [TopologicalSpace α]
Full source 
/-- A space is totally disconnected if all of its connected components are singletons. -/
@[mk_iff]
class TotallyDisconnectedSpace (α : Type u) [TopologicalSpace α] : Prop where
  /-- The universal set `Set.univ` in a totally disconnected space is totally disconnected. -/
  isTotallyDisconnected_univ : IsTotallyDisconnected (univ : Set α)
Totally disconnected space
Informal description
A topological space $X$ is called *totally disconnected* if every connected component of $X$ is a singleton. In other words, the only connected subsets of $X$ are the single-point sets.
IsPreconnected.subsingleton theorem
[TotallyDisconnectedSpace α] {s : Set α} (h : IsPreconnected s) : s.Subsingleton
Full source 
theorem IsPreconnected.subsingleton [TotallyDisconnectedSpace α] {s : Set α}
    (h : IsPreconnected s) : s.Subsingleton :=
  TotallyDisconnectedSpace.isTotallyDisconnected_univ s (subset_univ s) h
Preconnected subsets in totally disconnected spaces are singletons
Informal description
Let $\alpha$ be a totally disconnected topological space and $s$ be a preconnected subset of $\alpha$. Then $s$ is a subsingleton, i.e., it contains at most one point.
Pi.totallyDisconnectedSpace instance
{α : Type*} {β : α → Type*} [∀ a, TopologicalSpace (β a)] [∀ a, TotallyDisconnectedSpace (β a)] : TotallyDisconnectedSpace (∀ a : α, β a)
Full source 
instance Pi.totallyDisconnectedSpace {α : Type*} {β : α → Type*}
    [∀ a, TopologicalSpace (β a)] [∀ a, TotallyDisconnectedSpace (β a)] :
    TotallyDisconnectedSpace (∀ a : α, β a) :=
  ⟨fun t _ h2 =>
    have this : ∀ a, IsPreconnected ((fun x : ∀ a, β a => x a) '' t) := fun a =>
      h2.image (fun x => x a) (continuous_apply a).continuousOn
    fun x x_in y y_in => funext fun a => (this a).subsingleton ⟨x, x_in, rfl⟩ ⟨y, y_in, rfl⟩⟩
Product of Totally Disconnected Spaces is Totally Disconnected
Informal description
For any family of topological spaces $\{β_a\}_{a \in \alpha}$ where each $β_a$ is totally disconnected, the product space $\prod_{a \in \alpha} β_a$ equipped with the product topology is also totally disconnected. That is, the only connected subsets of the product space are singletons.
Prod.totallyDisconnectedSpace instance
[TopologicalSpace β] [TotallyDisconnectedSpace α] [TotallyDisconnectedSpace β] : TotallyDisconnectedSpace (α × β)
Full source 
instance Prod.totallyDisconnectedSpace [TopologicalSpace β] [TotallyDisconnectedSpace α]
    [TotallyDisconnectedSpace β] : TotallyDisconnectedSpace (α × β) :=
  ⟨fun t _ h2 =>
    have H1 : IsPreconnected (Prod.fst '' t) := h2.image Prod.fst continuous_fst.continuousOn
    have H2 : IsPreconnected (Prod.snd '' t) := h2.image Prod.snd continuous_snd.continuousOn
    fun x hx y hy =>
    Prod.ext (H1.subsingleton ⟨x, hx, rfl⟩ ⟨y, hy, rfl⟩)
      (H2.subsingleton ⟨x, hx, rfl⟩ ⟨y, hy, rfl⟩)⟩
Product of Totally Disconnected Spaces is Totally Disconnected
Informal description
For any topological spaces $\alpha$ and $\beta$ that are totally disconnected, the product space $\alpha \times \beta$ is also totally disconnected. That is, every connected component of $\alpha \times \beta$ is a singleton.
instTotallyDisconnectedSpaceSum instance
[TopologicalSpace β] [TotallyDisconnectedSpace α] [TotallyDisconnectedSpace β] : TotallyDisconnectedSpace (α ⊕ β)
Full source 
instance [TopologicalSpace β] [TotallyDisconnectedSpace α] [TotallyDisconnectedSpace β] :
    TotallyDisconnectedSpace (α ⊕ β) := by
  refine ⟨fun s _ hs => ?_⟩
  obtain ⟨t, ht, rfl⟩ | ⟨t, ht, rfl⟩ := Sum.isPreconnected_iff.1 hs
  · exact ht.subsingleton.image _
  · exact ht.subsingleton.image _
Disjoint Union of Totally Disconnected Spaces is Totally Disconnected
Informal description
For any topological spaces $\alpha$ and $\beta$ that are totally disconnected, the disjoint union $\alpha \oplus \beta$ is also totally disconnected. That is, every connected component of $\alpha \oplus \beta$ is a singleton.
instTotallyDisconnectedSpaceSigma instance
[∀ i, TopologicalSpace (π i)] [∀ i, TotallyDisconnectedSpace (π i)] : TotallyDisconnectedSpace (Σ i, π i)
Full source 
instance [∀ i, TopologicalSpace (π i)] [∀ i, TotallyDisconnectedSpace (π i)] :
    TotallyDisconnectedSpace (Σi, π i) := by
  refine ⟨fun s _ hs => ?_⟩
  obtain rfl | h := s.eq_empty_or_nonempty
  · exact subsingleton_empty
  · obtain ⟨a, t, ht, rfl⟩ := Sigma.isConnected_iff.1 ⟨h, hs⟩
    exact ht.isPreconnected.subsingleton.image _
Disjoint Union of Totally Disconnected Spaces is Totally Disconnected
Informal description
For any family of topological spaces $\{\pi_i\}_{i \in \iota}$ indexed by a type $\iota$, if each $\pi_i$ is totally disconnected, then the disjoint union $\Sigma_{i \in \iota} \pi_i$ is also totally disconnected. That is, every connected component of the disjoint union is a singleton.
totallyDisconnectedSpace_iff_connectedComponent_subsingleton theorem
: TotallyDisconnectedSpace α ↔ ∀ x : α, (connectedComponent x).Subsingleton
Full source 
/-- A space is totally disconnected iff its connected components are subsingletons. -/
theorem totallyDisconnectedSpace_iff_connectedComponent_subsingleton :
    TotallyDisconnectedSpaceTotallyDisconnectedSpace α ↔ ∀ x : α, (connectedComponent x).Subsingleton := by
  constructor
  · intro h x
    apply h.1
    · exact subset_univ _
    exact isPreconnected_connectedComponent
  intro h; constructor
  intro s s_sub hs
  rcases eq_empty_or_nonempty s with (rfl | ⟨x, x_in⟩)
  · exact subsingleton_empty
  · exact (h x).anti (hs.subset_connectedComponent x_in)
Characterization of Totally Disconnected Spaces via Subsingleton Connected Components
Informal description
A topological space $\alpha$ is totally disconnected if and only if for every point $x \in \alpha$, the connected component of $x$ is a subsingleton (i.e., contains at most one point).
totallyDisconnectedSpace_iff_connectedComponent_singleton theorem
: TotallyDisconnectedSpace α ↔ ∀ x : α, connectedComponent x = { x }
Full source 
/-- A space is totally disconnected iff its connected components are singletons. -/
theorem totallyDisconnectedSpace_iff_connectedComponent_singleton :
    TotallyDisconnectedSpaceTotallyDisconnectedSpace α ↔ ∀ x : α, connectedComponent x = {x} := by
  rw [totallyDisconnectedSpace_iff_connectedComponent_subsingleton]
  refine forall_congr' fun x => ?_
  rw [subsingleton_iff_singleton]
  exact mem_connectedComponent
Characterization of Totally Disconnected Spaces via Singleton Connected Components
Informal description
A topological space $\alpha$ is totally disconnected if and only if for every point $x \in \alpha$, the connected component of $x$ is the singleton set $\{x\}$.
connectedComponent_eq_singleton theorem
[TotallyDisconnectedSpace α] (x : α) : connectedComponent x = { x }
Full source 
@[simp] theorem connectedComponent_eq_singleton [TotallyDisconnectedSpace α] (x : α) :
    connectedComponent x = {x} :=
  totallyDisconnectedSpace_iff_connectedComponent_singleton.1 ‹_› x
Connected Components in Totally Disconnected Spaces are Singletons
Informal description
In a totally disconnected topological space $\alpha$, the connected component of any point $x \in \alpha$ is the singleton set $\{x\}$.
Continuous.image_connectedComponent_eq_singleton theorem
{β : Type*} [TopologicalSpace β] [TotallyDisconnectedSpace β] {f : α → β} (h : Continuous f) (a : α) : f '' connectedComponent a = {f a}
Full source 
/-- The image of a connected component in a totally disconnected space is a singleton. -/
@[simp]
theorem Continuous.image_connectedComponent_eq_singleton {β : Type*} [TopologicalSpace β]
    [TotallyDisconnectedSpace β] {f : α → β} (h : Continuous f) (a : α) :
    f '' connectedComponent a = {f a} :=
  (Set.subsingleton_iff_singleton <| mem_image_of_mem f mem_connectedComponent).mp
    (isPreconnected_connectedComponent.image f h.continuousOn).subsingleton
Continuous Image of Connected Component in Totally Disconnected Space is Singleton
Informal description
Let $\alpha$ and $\beta$ be topological spaces with $\beta$ totally disconnected. For any continuous function $f \colon \alpha \to \beta$ and any point $a \in \alpha$, the image of the connected component of $a$ under $f$ is the singleton set $\{f(a)\}$.
isTotallyDisconnected_of_totallyDisconnectedSpace theorem
[TotallyDisconnectedSpace α] (s : Set α) : IsTotallyDisconnected s
Full source 
theorem isTotallyDisconnected_of_totallyDisconnectedSpace [TotallyDisconnectedSpace α] (s : Set α) :
    IsTotallyDisconnected s := fun t _ ht =>
  TotallyDisconnectedSpace.isTotallyDisconnected_univ _ t.subset_univ ht
Subsets of a totally disconnected space are totally disconnected
Informal description
Let $\alpha$ be a topological space that is totally disconnected. Then any subset $s \subseteq \alpha$ is totally disconnected. That is, every nonempty connected subset of $s$ is a singleton.
isTotallyDisconnected_of_image theorem
[TopologicalSpace β] {f : α → β} (hf : ContinuousOn f s) (hf' : Injective f) (h : IsTotallyDisconnected (f '' s)) : IsTotallyDisconnected s
Full source 
theorem isTotallyDisconnected_of_image [TopologicalSpace β] {f : α → β} (hf : ContinuousOn f s)
    (hf' : Injective f) (h : IsTotallyDisconnected (f '' s)) : IsTotallyDisconnected s :=
  fun _t hts ht _x x_in _y y_in =>
  hf' <|
    h _ (image_subset f hts) (ht.image f <| hf.mono hts) (mem_image_of_mem f x_in)
      (mem_image_of_mem f y_in)
Total Disconnectedness is Preserved under Continuous Injective Images
Informal description
Let $X$ and $Y$ be topological spaces, $s \subseteq X$ a subset, and $f \colon X \to Y$ a function that is continuous on $s$ and injective. If the image $f(s)$ is totally disconnected in $Y$, then $s$ is totally disconnected in $X$.
Topology.IsEmbedding.isTotallyDisconnected theorem
[TopologicalSpace β] {f : α → β} {s : Set α} (hf : IsEmbedding f) (h : IsTotallyDisconnected (f '' s)) : IsTotallyDisconnected s
Full source 
lemma Topology.IsEmbedding.isTotallyDisconnected [TopologicalSpace β] {f : α → β} {s : Set α}
    (hf : IsEmbedding f) (h : IsTotallyDisconnected (f '' s)) : IsTotallyDisconnected s :=
  isTotallyDisconnected_of_image hf.continuous.continuousOn hf.injective h
Total Disconnectedness is Preserved under Topological Embeddings
Informal description
Let $X$ and $Y$ be topological spaces, $s \subseteq X$ a subset, and $f \colon X \to Y$ a topological embedding. If the image $f(s)$ is totally disconnected in $Y$, then $s$ is totally disconnected in $X$.
Topology.IsEmbedding.isTotallyDisconnected_image theorem
[TopologicalSpace β] {f : α → β} {s : Set α} (hf : IsEmbedding f) : IsTotallyDisconnected (f '' s) ↔ IsTotallyDisconnected s
Full source 
lemma Topology.IsEmbedding.isTotallyDisconnected_image [TopologicalSpace β] {f : α → β} {s : Set α}
    (hf : IsEmbedding f) : IsTotallyDisconnectedIsTotallyDisconnected (f '' s) ↔ IsTotallyDisconnected s := by
  refine ⟨hf.isTotallyDisconnected, fun hs u hus hu ↦ ?_⟩
  obtain ⟨v, hvs, rfl⟩ : ∃ v, v ⊆ s ∧ f '' v = u :=
    ⟨f ⁻¹' u ∩ s, inter_subset_right, by rwa [image_preimage_inter, inter_eq_left]⟩
  rw [hf.isInducing.isPreconnected_image] at hu
  exact (hs v hvs hu).image _
Total Disconnectedness is Preserved under Topological Embeddings (Image Version)
Informal description
Let $X$ and $Y$ be topological spaces, $s \subseteq X$ a subset, and $f \colon X \to Y$ a topological embedding. Then the image $f(s)$ is totally disconnected in $Y$ if and only if $s$ is totally disconnected in $X$.
Topology.IsEmbedding.isTotallyDisconnected_range theorem
[TopologicalSpace β] {f : α → β} (hf : IsEmbedding f) : IsTotallyDisconnected (range f) ↔ TotallyDisconnectedSpace α
Full source 
lemma Topology.IsEmbedding.isTotallyDisconnected_range [TopologicalSpace β] {f : α → β}
    (hf : IsEmbedding f) : IsTotallyDisconnectedIsTotallyDisconnected (range f) ↔ TotallyDisconnectedSpace α := by
  rw [totallyDisconnectedSpace_iff, ← image_univ, hf.isTotallyDisconnected_image]
Total Disconnectedness of Range under Embedding Equivalence to Totally Disconnected Space
Informal description
Let $X$ and $Y$ be topological spaces, and let $f \colon X \to Y$ be a topological embedding. Then the range of $f$ is totally disconnected in $Y$ if and only if $X$ is a totally disconnected space.
totallyDisconnectedSpace_subtype_iff theorem
{s : Set α} : TotallyDisconnectedSpace s ↔ IsTotallyDisconnected s
Full source 
lemma totallyDisconnectedSpace_subtype_iff {s : Set α} :
    TotallyDisconnectedSpaceTotallyDisconnectedSpace s ↔ IsTotallyDisconnected s := by
  rw [← IsEmbedding.subtypeVal.isTotallyDisconnected_range, Subtype.range_val]
Equivalence of Totally Disconnected Subspace and Totally Disconnected Subset
Informal description
For any subset $s$ of a topological space $\alpha$, the subspace $s$ is a totally disconnected space if and only if $s$ is a totally disconnected subset of $\alpha$. Here, a *totally disconnected space* means that every connected component is a singleton, and a *totally disconnected subset* means that every nonempty preconnected subset is a singleton.
Subtype.totallyDisconnectedSpace instance
{α : Type*} {p : α → Prop} [TopologicalSpace α] [TotallyDisconnectedSpace α] : TotallyDisconnectedSpace (Subtype p)
Full source 
instance Subtype.totallyDisconnectedSpace {α : Type*} {p : α → Prop} [TopologicalSpace α]
    [TotallyDisconnectedSpace α] : TotallyDisconnectedSpace (Subtype p) :=
  totallyDisconnectedSpace_subtype_iff.2 (isTotallyDisconnected_of_totallyDisconnectedSpace _)
Subtypes of Totally Disconnected Spaces are Totally Disconnected
Informal description
For any topological space $\alpha$ that is totally disconnected and any predicate $p : \alpha \to \mathrm{Prop}$, the subtype $\{x \in \alpha \mid p(x)\}$ is also a totally disconnected space. Here, a *totally disconnected space* means that every connected component is a singleton.
IsTotallySeparated definition
(s : Set α) : Prop
Full source 
/-- A set `s` is called totally separated if any two points of this set can be separated
by two disjoint open sets covering `s`. -/
def IsTotallySeparated (s : Set α) : Prop :=
  Set.Pairwise s fun x y =>
  ∃ u v : Set α, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ s ⊆ u ∪ v ∧ Disjoint u v
Totally separated set
Informal description
A subset $s$ of a topological space $\alpha$ is called *totally separated* if for any two distinct points $x, y \in s$, there exist disjoint open sets $u$ and $v$ such that: - $x \in u$ and $y \in v$, - $s$ is contained in the union $u \cup v$. In other words, any two points in $s$ can be separated by disjoint open sets that together cover $s$.
isTotallySeparated_empty theorem
: IsTotallySeparated (∅ : Set α)
Full source 
theorem isTotallySeparated_empty : IsTotallySeparated (∅ : Set α) := fun _ => False.elim
Empty Set is Totally Separated
Informal description
The empty set $\emptyset$ in a topological space $\alpha$ is totally separated.
isTotallySeparated_singleton theorem
{x} : IsTotallySeparated ({ x } : Set α)
Full source 
theorem isTotallySeparated_singleton {x} : IsTotallySeparated ({x} : Set α) := fun _ hp _ hq hpq =>
  (hpq <| (eq_of_mem_singleton hp).symm ▸ (eq_of_mem_singleton hq).symm).elim
Singleton sets are totally separated
Informal description
For any topological space $\alpha$ and any point $x \in \alpha$, the singleton set $\{x\}$ is totally separated. That is, for any two distinct points in $\{x\}$ (which is only possible if they are equal, hence vacuously true), there exist disjoint open sets containing each point respectively and covering $\{x\}$.
isTotallyDisconnected_of_isTotallySeparated theorem
{s : Set α} (H : IsTotallySeparated s) : IsTotallyDisconnected s
Full source 
theorem isTotallyDisconnected_of_isTotallySeparated {s : Set α} (H : IsTotallySeparated s) :
    IsTotallyDisconnected s := by
  intro t hts ht x x_in y y_in
  by_contra h
  obtain
    ⟨u : Set α, v : Set α, hu : IsOpen u, hv : IsOpen v, hxu : x ∈ u, hyv : y ∈ v, hs : s ⊆ u ∪ v,
      huv⟩ :=
    H (hts x_in) (hts y_in) h
  refine (ht _ _ hu hv (hts.trans hs) ⟨x, x_in, hxu⟩ ⟨y, y_in, hyv⟩).ne_empty ?_
  rw [huv.inter_eq, inter_empty]
Totally separated implies totally disconnected
Informal description
For any subset $s$ of a topological space $\alpha$, if $s$ is totally separated, then it is totally disconnected. That is, if for any two distinct points $x, y \in s$ there exist disjoint open sets $u$ and $v$ such that $x \in u$, $y \in v$, and $s \subseteq u \cup v$, then every connected component of $s$ is a singleton.
TotallySeparatedSpace structure
(α : Type u) [TopologicalSpace α]
Full source 
/-- A space is totally separated if any two points can be separated by two disjoint open sets
covering the whole space. -/
@[mk_iff] class TotallySeparatedSpace (α : Type u) [TopologicalSpace α] : Prop where
  /-- The universal set `Set.univ` in a totally separated space is totally separated. -/
  isTotallySeparated_univ : IsTotallySeparated (univ : Set α)
Totally separated topological space
Informal description
A topological space $\alpha$ is called *totally separated* if for any two distinct points $x$ and $y$ in $\alpha$, there exist disjoint open sets $U$ and $V$ such that $x \in U$, $y \in V$, and $U \cup V$ covers the entire space $\alpha$.
TotallySeparatedSpace.totallyDisconnectedSpace instance
(α : Type u) [TopologicalSpace α] [TotallySeparatedSpace α] : TotallyDisconnectedSpace α
Full source 
instance (priority := 100) TotallySeparatedSpace.totallyDisconnectedSpace (α : Type u)
    [TopologicalSpace α] [TotallySeparatedSpace α] : TotallyDisconnectedSpace α :=
  ⟨TotallySeparatedSpace.isTotallySeparated_univ.isTotallyDisconnected⟩
Totally Separated Implies Totally Disconnected
Informal description
Every totally separated topological space is totally disconnected.
TotallySeparatedSpace.of_discrete instance
(α : Type*) [TopologicalSpace α] [DiscreteTopology α] : TotallySeparatedSpace α
Full source 
instance (priority := 100) TotallySeparatedSpace.of_discrete (α : Type*) [TopologicalSpace α]
    [DiscreteTopology α] : TotallySeparatedSpace α :=
  ⟨fun _ _ b _ h => ⟨{b}ᶜ, {b}, isOpen_discrete _, isOpen_discrete _, h, rfl,
    (compl_union_self _).symm.subset, disjoint_compl_left⟩⟩
Discrete Spaces are Totally Separated
Informal description
Every discrete topological space is totally separated. That is, for any type $\alpha$ equipped with the discrete topology, the space $\alpha$ satisfies the property that any two distinct points can be separated by disjoint open sets whose union is the whole space.
totallySeparatedSpace_iff_exists_isClopen theorem
{α : Type*} [TopologicalSpace α] : TotallySeparatedSpace α ↔ Pairwise (∃ U : Set α, IsClopen U ∧ · ∈ U ∧ · ∈ Uᶜ)
Full source 
theorem totallySeparatedSpace_iff_exists_isClopen {α : Type*} [TopologicalSpace α] :
    TotallySeparatedSpaceTotallySeparatedSpace α ↔ Pairwise (∃ U : Set α, IsClopen U ∧ · ∈ U ∧ · ∈ Uᶜ) := by
  simp only [totallySeparatedSpace_iff, IsTotallySeparated, Set.Pairwise, mem_univ, true_implies]
  refine forall₃_congr fun x y _ ↦
    ⟨fun ⟨U, V, hU, hV, Ux, Vy, f, disj⟩ ↦ ?_, fun ⟨U, hU, Ux, Ucy⟩ ↦ ?_⟩
  · exact ⟨U, isClopen_of_disjoint_cover_open f hU hV disj,
      Ux, fun Uy ↦ Set.disjoint_iff.mp disj ⟨Uy, Vy⟩⟩
  · exact ⟨U, Uᶜ, hU.2, hU.compl.2, Ux, Ucy, (Set.union_compl_self U).ge, disjoint_compl_right⟩
Characterization of Totally Separated Spaces via Clopen Sets
Informal description
A topological space $\alpha$ is totally separated if and only if for every pair of distinct points $x$ and $y$ in $\alpha$, there exists a clopen set $U$ such that $x \in U$ and $y \in U^c$.
exists_isClopen_of_totally_separated theorem
{α : Type*} [TopologicalSpace α] [TotallySeparatedSpace α] : Pairwise (∃ U : Set α, IsClopen U ∧ · ∈ U ∧ · ∈ Uᶜ)
Full source 
theorem exists_isClopen_of_totally_separated {α : Type*} [TopologicalSpace α]
    [TotallySeparatedSpace α] : Pairwise (∃ U : Set α, IsClopen U ∧ · ∈ U ∧ · ∈ Uᶜ) :=
  totallySeparatedSpace_iff_exists_isClopen.mp ‹_›
Existence of Clopen Separators in Totally Separated Spaces
Informal description
Let $\alpha$ be a topological space that is totally separated. Then for any two distinct points $x$ and $y$ in $\alpha$, there exists a clopen set $U$ such that $x \in U$ and $y \in U^c$.
isTotallyDisconnected_of_isClopen_set theorem
{X : Type*} [TopologicalSpace X] (hX : Pairwise (∃ (U : Set X), IsClopen U ∧ · ∈ U ∧ · ∉ U)) : IsTotallyDisconnected (Set.univ : Set X)
Full source 
/-- Let `X` be a topological space, and suppose that for all distinct `x,y ∈ X`, there
  is some clopen set `U` such that `x ∈ U` and `y ∉ U`. Then `X` is totally disconnected. -/
@[deprecated totallySeparatedSpace_iff_exists_isClopen (since := "2025-04-03")]
theorem isTotallyDisconnected_of_isClopen_set {X : Type*} [TopologicalSpace X]
    (hX : Pairwise (∃ (U : Set X), IsClopen U ∧ · ∈ U ∧ · ∉ U)) :
    IsTotallyDisconnected (Set.univ : Set X) :=
  (totallySeparatedSpace_iff X).mp (totallySeparatedSpace_iff_exists_isClopen.mpr hX)
    |>.isTotallyDisconnected
Clopen Separation Implies Total Disconnectedness
Informal description
Let $X$ be a topological space. Suppose that for every pair of distinct points $x, y \in X$, there exists a clopen set $U$ such that $x \in U$ and $y \notin U$. Then $X$ is totally disconnected, i.e., every nonempty connected subset of $X$ is a singleton.
Continuous.image_eq_of_connectedComponent_eq theorem
(h : Continuous f) (a b : α) (hab : connectedComponent a = connectedComponent b) : f a = f b
Full source 
theorem Continuous.image_eq_of_connectedComponent_eq (h : Continuous f) (a b : α)
    (hab : connectedComponent a = connectedComponent b) : f a = f b :=
  singleton_eq_singleton_iff.1 <|
    h.image_connectedComponent_eq_singleton a ▸
      h.image_connectedComponent_eq_singleton b ▸ hab ▸ rfl
Continuous Functions Agree on Points in the Same Connected Component
Informal description
Let $f \colon \alpha \to \beta$ be a continuous function between topological spaces. For any two points $a, b \in \alpha$ with the same connected component (i.e., $\text{connectedComponent}(a) = \text{connectedComponent}(b)$), we have $f(a) = f(b)$.
Continuous.connectedComponentsLift definition
(h : Continuous f) : ConnectedComponents α → β
Full source 
/--
The lift to `connectedComponents α` of a continuous map from `α` to a totally disconnected space
-/
def Continuous.connectedComponentsLift (h : Continuous f) : ConnectedComponents α → β := fun x =>
  Quotient.liftOn' x f h.image_eq_of_connectedComponent_eq
Lift of a continuous function to connected components in a totally disconnected space
Informal description
Given a continuous function $f \colon \alpha \to \beta$ where $\beta$ is a totally disconnected space, the function `connectedComponentsLift` lifts $f$ to a function from the connected components of $\alpha$ to $\beta$. Specifically, for any connected component $[x] \in \text{ConnectedComponents}(\alpha)$, the lift is defined as $f(x)$, which is well-defined since $f$ is constant on each connected component.
Continuous.connectedComponentsLift_continuous theorem
(h : Continuous f) : Continuous h.connectedComponentsLift
Full source 
@[continuity]
theorem Continuous.connectedComponentsLift_continuous (h : Continuous f) :
    Continuous h.connectedComponentsLift :=
  h.quotient_liftOn' <| by convert h.image_eq_of_connectedComponent_eq
Continuity of the Lift to Connected Components for Totally Disconnected Codomain
Informal description
Let $f \colon \alpha \to \beta$ be a continuous function between topological spaces, where $\beta$ is totally disconnected. Then the lifted function $h.\text{connectedComponentsLift} \colon \text{ConnectedComponents}(\alpha) \to \beta$ is continuous.
Continuous.connectedComponentsLift_apply_coe theorem
(h : Continuous f) (x : α) : h.connectedComponentsLift x = f x
Full source 
@[simp]
theorem Continuous.connectedComponentsLift_apply_coe (h : Continuous f) (x : α) :
    h.connectedComponentsLift x = f x :=
  rfl
Evaluation of Continuous Lift on Connected Components
Informal description
Let $X$ and $Y$ be topological spaces with $Y$ totally disconnected, and let $f \colon X \to Y$ be a continuous function. For any point $x \in X$, the lift of $f$ to the connected components space satisfies $h.\text{connectedComponentsLift}([x]) = f(x)$, where $[x]$ denotes the connected component of $x$ in $X$.
Continuous.connectedComponentsLift_comp_coe theorem
(h : Continuous f) : h.connectedComponentsLift ∘ (↑) = f
Full source 
@[simp]
theorem Continuous.connectedComponentsLift_comp_coe (h : Continuous f) :
    h.connectedComponentsLift ∘ (↑) = f :=
  rfl
Lifted Function Composed with Projection Equals Original Function
Informal description
Given a continuous function $f \colon \alpha \to \beta$ where $\beta$ is a totally disconnected space, the composition of the lifted function $h.\text{connectedComponentsLift}$ with the canonical projection $\pi \colon \alpha \to \text{ConnectedComponents}(\alpha)$ equals $f$, i.e., $h.\text{connectedComponentsLift} \circ \pi = f$.
connectedComponents_lift_unique' theorem
{β : Sort*} {g₁ g₂ : ConnectedComponents α → β} (hg : g₁ ∘ ((↑) : α → ConnectedComponents α) = g₂ ∘ (↑)) : g₁ = g₂
Full source 
theorem connectedComponents_lift_unique' {β : Sort*} {g₁ g₂ : ConnectedComponents α → β}
    (hg : g₁ ∘ ((↑) : α → ConnectedComponents α) = g₂ ∘ (↑)) : g₁ = g₂ :=
  ConnectedComponents.surjective_coe.injective_comp_right hg
Uniqueness of Lifts to Connected Components
Informal description
Let $\alpha$ be a topological space and $\beta$ be any type. For any two functions $g_1, g_2 \colon \text{ConnectedComponents}(\alpha) \to \beta$, if $g_1 \circ \pi = g_2 \circ \pi$ where $\pi \colon \alpha \to \text{ConnectedComponents}(\alpha)$ is the canonical projection map, then $g_1 = g_2$.
Continuous.connectedComponentsLift_unique theorem
(h : Continuous f) (g : ConnectedComponents α → β) (hg : g ∘ (↑) = f) : g = h.connectedComponentsLift
Full source 
theorem Continuous.connectedComponentsLift_unique (h : Continuous f) (g : ConnectedComponents α → β)
    (hg : g ∘ (↑) = f) : g = h.connectedComponentsLift :=
  connectedComponents_lift_unique' <| hg.trans h.connectedComponentsLift_comp_coe.symm
Uniqueness of the Lift to Connected Components for Continuous Functions into Totally Disconnected Spaces
Informal description
Let $\alpha$ and $\beta$ be topological spaces, with $\beta$ totally disconnected. Given a continuous function $f \colon \alpha \to \beta$ and a function $g \colon \text{ConnectedComponents}(\alpha) \to \beta$ such that $g \circ \pi = f$, where $\pi \colon \alpha \to \text{ConnectedComponents}(\alpha)$ is the canonical projection, then $g$ must be equal to the lift of $f$ to the connected components, i.e., $g = h.\text{connectedComponentsLift}$.
ConnectedComponents.totallyDisconnectedSpace instance
: TotallyDisconnectedSpace (ConnectedComponents α)
Full source 
instance ConnectedComponents.totallyDisconnectedSpace :
    TotallyDisconnectedSpace (ConnectedComponents α) := by
  rw [totallyDisconnectedSpace_iff_connectedComponent_singleton]
  refine ConnectedComponents.surjective_coe.forall.2 fun x => ?_
  rw [← ConnectedComponents.isQuotientMap_coe.image_connectedComponent, ←
    connectedComponents_preimage_singleton, image_preimage_eq _ ConnectedComponents.surjective_coe]
  refine ConnectedComponents.surjective_coe.forall.2 fun y => ?_
  rw [connectedComponents_preimage_singleton]
  exact isConnected_connectedComponent
Connected Components Space is Totally Disconnected
Informal description
The space of connected components of a topological space $\alpha$ is totally disconnected, meaning every connected component in this space is a singleton set.
Continuous.connectedComponentsMap definition
{β : Type*} [TopologicalSpace β] {f : α → β} (h : Continuous f) : ConnectedComponents α → ConnectedComponents β
Full source 
/-- Functoriality of `connectedComponents` -/
def Continuous.connectedComponentsMap {β : Type*} [TopologicalSpace β] {f : α → β}
    (h : Continuous f) : ConnectedComponents α → ConnectedComponents β :=
  Continuous.connectedComponentsLift (ConnectedComponents.continuous_coe.comp h)
Induced map on connected components by a continuous function
Informal description
Given a continuous function $f \colon \alpha \to \beta$ between topological spaces, the function `connectedComponentsMap` maps a connected component $[x]$ in $\alpha$ to the connected component $[f(x)]$ in $\beta$. This is well-defined because continuous functions preserve connectedness.
Continuous.connectedComponentsMap_continuous theorem
{β : Type*} [TopologicalSpace β] {f : α → β} (h : Continuous f) : Continuous h.connectedComponentsMap
Full source 
theorem Continuous.connectedComponentsMap_continuous {β : Type*} [TopologicalSpace β] {f : α → β}
    (h : Continuous f) : Continuous h.connectedComponentsMap :=
  Continuous.connectedComponentsLift_continuous (ConnectedComponents.continuous_coe.comp h)
Continuity of the Induced Map on Connected Components
Informal description
Let $X$ and $Y$ be topological spaces, and let $f \colon X \to Y$ be a continuous function. Then the induced map $\text{ConnectedComponents}(f) \colon \text{ConnectedComponents}(X) \to \text{ConnectedComponents}(Y)$ is continuous.
IsPreconnected.constant theorem
{Y : Type*} [TopologicalSpace Y] [DiscreteTopology Y] {s : Set α} (hs : IsPreconnected s) {f : α → Y} (hf : ContinuousOn f s) {x y : α} (hx : x ∈ s) (hy : y ∈ s) : f x = f y
Full source 
/-- A preconnected set `s` has the property that every map to a
discrete space that is continuous on `s` is constant on `s` -/
theorem IsPreconnected.constant {Y : Type*} [TopologicalSpace Y] [DiscreteTopology Y] {s : Set α}
    (hs : IsPreconnected s) {f : α → Y} (hf : ContinuousOn f s) {x y : α} (hx : x ∈ s)
    (hy : y ∈ s) : f x = f y :=
  (hs.image f hf).subsingleton (mem_image_of_mem f hx) (mem_image_of_mem f hy)
Constant Function Property on Preconnected Sets in Discrete Codomain
Informal description
Let $X$ and $Y$ be topological spaces with $Y$ discrete, $s \subseteq X$ a preconnected subset, and $f \colon X \to Y$ a function that is continuous on $s$. Then for any two points $x, y \in s$, the function values coincide, i.e., $f(x) = f(y)$.
PreconnectedSpace.constant theorem
{Y : Type*} [TopologicalSpace Y] [DiscreteTopology Y] (hp : PreconnectedSpace α) {f : α → Y} (hf : Continuous f) {x y : α} : f x = f y
Full source 
/-- A `PreconnectedSpace` version of `isPreconnected.constant` -/
theorem PreconnectedSpace.constant {Y : Type*} [TopologicalSpace Y] [DiscreteTopology Y]
    (hp : PreconnectedSpace α) {f : α → Y} (hf : Continuous f) {x y : α} : f x = f y :=
  IsPreconnected.constant hp.isPreconnected_univ (Continuous.continuousOn hf) trivial trivial
Constant Function Property on Preconnected Spaces with Discrete Codomain
Informal description
Let $X$ and $Y$ be topological spaces with $Y$ discrete, and suppose $X$ is preconnected. For any continuous function $f \colon X \to Y$ and any two points $x, y \in X$, the function values coincide, i.e., $f(x) = f(y)$.
IsPreconnected.constant_of_mapsTo theorem
{S : Set α} (hS : IsPreconnected S) {β} [TopologicalSpace β] {T : Set β} [DiscreteTopology T] {f : α → β} (hc : ContinuousOn f S) (hTm : MapsTo f S T) {x y : α} (hx : x ∈ S) (hy : y ∈ S) : f x = f y
Full source 
/-- Refinement of `IsPreconnected.constant` only assuming the map factors through a
discrete subset of the target. -/
theorem IsPreconnected.constant_of_mapsTo {S : Set α} (hS : IsPreconnected S)
    {β} [TopologicalSpace β] {T : Set β} [DiscreteTopology T] {f : α → β} (hc : ContinuousOn f S)
    (hTm : MapsTo f S T) {x y : α} (hx : x ∈ S) (hy : y ∈ S) : f x = f y := by
  let F : S → T := hTm.restrict f S T
  suffices F ⟨x, hx⟩ = F ⟨y, hy⟩ by rwa [← Subtype.coe_inj] at this
  exact (isPreconnected_iff_preconnectedSpace.mp hS).constant (hc.restrict_mapsTo _)
Constant Function Property on Preconnected Sets with Discrete Image
Informal description
Let $S$ be a preconnected subset of a topological space $\alpha$, and let $T$ be a subset of a topological space $\beta$ with the discrete topology. For any function $f \colon \alpha \to \beta$ that is continuous on $S$ and maps $S$ into $T$, and for any two points $x, y \in S$, the function values coincide, i.e., $f(x) = f(y)$.
IsPreconnected.eqOn_const_of_mapsTo theorem
{S : Set α} (hS : IsPreconnected S) {β} [TopologicalSpace β] {T : Set β} [DiscreteTopology T] {f : α → β} (hc : ContinuousOn f S) (hTm : MapsTo f S T) (hne : T.Nonempty) : ∃ y ∈ T, EqOn f (const α y) S
Full source 
/-- A version of `IsPreconnected.constant_of_mapsTo` that assumes that the codomain is nonempty and
proves that `f` is equal to `const α y` on `S` for some `y ∈ T`. -/
theorem IsPreconnected.eqOn_const_of_mapsTo {S : Set α} (hS : IsPreconnected S)
    {β} [TopologicalSpace β] {T : Set β} [DiscreteTopology T] {f : α → β} (hc : ContinuousOn f S)
    (hTm : MapsTo f S T) (hne : T.Nonempty) : ∃ y ∈ T, EqOn f (const α y) S := by
  rcases S.eq_empty_or_nonempty with (rfl | ⟨x, hx⟩)
  · exact hne.imp fun _ hy => ⟨hy, eqOn_empty _ _⟩
  · exact ⟨f x, hTm hx, fun x' hx' => hS.constant_of_mapsTo hc hTm hx' hx⟩
Constant Function Property on Preconnected Sets with Nonempty Discrete Image
Informal description
Let $S$ be a preconnected subset of a topological space $\alpha$, and let $T$ be a nonempty subset of a topological space $\beta$ with the discrete topology. For any function $f \colon \alpha \to \beta$ that is continuous on $S$ and maps $S$ into $T$, there exists a constant $y \in T$ such that $f$ coincides with the constant function $y$ on $S$, i.e., $f(x) = y$ for all $x \in S$.