# Documentation

Mathlib.Topology.Connected.TotallyDisconnected

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

def IsTotallyDisconnected {α : Type u} [] (s : Set α) :

A set s is called totally disconnected if every subset t ⊆ s which is preconnected is a subsingleton, ie either empty or a singleton.

Equations
• = ts,
Instances For
theorem isTotallyDisconnected_singleton {α : Type u} [] {x : α} :

A space is totally disconnected if all of its connected components are singletons.

• isTotallyDisconnected_univ : IsTotallyDisconnected Set.univ

The universal set Set.univ in a totally disconnected space is totally disconnected.

Instances
theorem IsPreconnected.subsingleton {α : Type u} [] {s : Set α} (h : ) :
instance Pi.totallyDisconnectedSpace {α : Type u_3} {β : αType u_4} [(a : α) → TopologicalSpace (β a)] [∀ (a : α), ] :
TotallyDisconnectedSpace ((a : α) → β a)
Equations
instance Prod.totallyDisconnectedSpace {α : Type u} {β : Type v} [] [] :
Equations
• (_ : ) = (_ : )
Equations
• (_ : ) = (_ : )
instance instTotallyDisconnectedSpaceSigmaInstTopologicalSpaceSigma {ι : Type u_1} {π : ιType u_2} [(i : ι) → TopologicalSpace (π i)] [∀ (i : ι), ] :
TotallyDisconnectedSpace ((i : ι) × π i)
Equations
theorem isTotallyDisconnected_of_isClopen_set {X : Type u_3} [] (hX : Pairwise fun (x y : X) => ∃ (U : Set X), x U yU) :

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.

A space is totally disconnected iff its connected components are subsingletons.

A space is totally disconnected iff its connected components are singletons.

@[simp]
theorem connectedComponent_eq_singleton {α : Type u} [] (x : α) :
= {x}
@[simp]
theorem Continuous.image_connectedComponent_eq_singleton {α : Type u} [] {β : Type u_3} [] {f : αβ} (h : ) (a : α) :
= {f a}

The image of a connected component in a totally disconnected space is a singleton.

theorem isTotallyDisconnected_of_image {α : Type u} {β : Type v} [] {s : Set α} [] {f : αβ} (hf : ) (hf' : ) (h : IsTotallyDisconnected (f '' s)) :
theorem Embedding.isTotallyDisconnected {α : Type u} {β : Type v} [] [] {f : αβ} (hf : ) {s : Set α} (h : IsTotallyDisconnected (f '' s)) :
theorem Embedding.isTotallyDisconnected_image {α : Type u} {β : Type v} [] [] {f : αβ} (hf : ) {s : Set α} :
theorem Embedding.isTotallyDisconnected_range {α : Type u} {β : Type v} [] [] {f : αβ} (hf : ) :
theorem totallyDisconnectedSpace_subtype_iff {α : Type u} [] {s : Set α} :
instance Subtype.totallyDisconnectedSpace {α : Type u_3} {p : αProp} [] :
Equations
def IsTotallySeparated {α : Type u} [] (s : Set α) :

A set s is called totally separated if any two points of this set can be separated by two disjoint open sets covering s.

Equations
Instances For
theorem isTotallySeparated_empty {α : Type u} [] :
theorem isTotallySeparated_singleton {α : Type u} [] {x : α} :
theorem isTotallyDisconnected_of_isTotallySeparated {α : Type u} [] {s : Set α} (H : ) :
theorem IsTotallySeparated.isTotallyDisconnected {α : Type u} [] {s : Set α} (H : ) :

Alias of isTotallyDisconnected_of_isTotallySeparated.

class TotallySeparatedSpace (α : Type u) [] :

A space is totally separated if any two points can be separated by two disjoint open sets covering the whole space.

• isTotallySeparated_univ : IsTotallySeparated Set.univ

The universal set Set.univ in a totally separated space is totally separated.

Instances
Equations
• (_ : ) = (_ : )
instance TotallySeparatedSpace.of_discrete (α : Type u_3) [] [] :
Equations
• (_ : ) = (_ : )
theorem exists_isClopen_of_totally_separated {α : Type u_3} [] {x : α} {y : α} (hxy : x y) :
∃ (U : Set α), x U y U
theorem Continuous.image_eq_of_connectedComponent_eq {α : Type u} {β : Type v} [] [] {f : αβ} (h : ) (a : α) (b : α) (hab : ) :
f a = f b
def Continuous.connectedComponentsLift {α : Type u} {β : Type v} [] [] {f : αβ} (h : ) :

The lift to connectedComponents α of a continuous map from α to a totally disconnected space

Equations
Instances For
theorem Continuous.connectedComponentsLift_continuous {α : Type u} {β : Type v} [] [] {f : αβ} (h : ) :
@[simp]
theorem Continuous.connectedComponentsLift_apply_coe {α : Type u} {β : Type v} [] [] {f : αβ} (h : ) (x : α) :
@[simp]
theorem Continuous.connectedComponentsLift_comp_coe {α : Type u} {β : Type v} [] [] {f : αβ} (h : ) :
ConnectedComponents.mk = f
theorem connectedComponents_lift_unique' {α : Type u} [] {β : Sort u_3} {g₁ : } {g₂ : } (hg : g₁ ConnectedComponents.mk = g₂ ConnectedComponents.mk) :
g₁ = g₂
theorem Continuous.connectedComponentsLift_unique {α : Type u} {β : Type v} [] [] {f : αβ} (h : ) (g : ) (hg : g ConnectedComponents.mk = f) :
Equations
def Continuous.connectedComponentsMap {α : Type u} [] {β : Type u_3} [] {f : αβ} (h : ) :

Functoriality of connectedComponents

Equations
Instances For
theorem Continuous.connectedComponentsMap_continuous {α : Type u} [] {β : Type u_3} [] {f : αβ} (h : ) :
theorem IsPreconnected.constant {α : Type u} [] {Y : Type u_3} [] [] {s : Set α} (hs : ) {f : αY} (hf : ) {x : α} {y : α} (hx : x s) (hy : y s) :
f x = f y

A preconnected set s has the property that every map to a discrete space that is continuous on s is constant on s

theorem PreconnectedSpace.constant {α : Type u} [] {Y : Type u_3} [] [] (hp : ) {f : αY} (hf : ) {x : α} {y : α} :
f x = f y

A PreconnectedSpace version of isPreconnected.constant

theorem IsPreconnected.constant_of_mapsTo {α : Type u} {β : Type v} [] [] {S : Set α} (hS : ) {T : Set β} [] {f : αβ} (hc : ) (hTm : Set.MapsTo f S T) {x : α} {y : α} (hx : x S) (hy : y S) :
f x = f y

Refinement of IsPreconnected.constant only assuming the map factors through a discrete subset of the target.

theorem IsPreconnected.eqOn_const_of_mapsTo {α : Type u} {β : Type v} [] [] {S : Set α} (hS : ) {T : Set β} [] {f : αβ} (hc : ) (hTm : Set.MapsTo f S T) (hne : ) :
∃ y ∈ T, Set.EqOn f () S

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.