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} [TopologicalSpace α] (s : Set α) : Prop

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

• IsTotallyDisconnected s = ∀ t ⊆ s, IsPreconnected t → t.Subsingleton

theorem isTotallyDisconnected_empty {α : Type u} [TopologicalSpace α] : IsTotallyDisconnected ∅

theorem isTotallyDisconnected_singleton {α : Type u} [TopologicalSpace α] {x : α} : IsTotallyDisconnected {x}

theorem totallyDisconnectedSpace_iff (α : Type u) [TopologicalSpace α] : TotallyDisconnectedSpace α ↔ IsTotallyDisconnected Set.univ

class TotallyDisconnectedSpace (α : Type u) [TopologicalSpace α] : Prop

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.

theorem TotallyDisconnectedSpace.isTotallyDisconnected_univ {α : Type u} [TopologicalSpace α] [self : TotallyDisconnectedSpace α] : IsTotallyDisconnected Set.univ

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

theorem IsPreconnected.subsingleton {α : Type u} [TopologicalSpace α] [TotallyDisconnectedSpace α] {s : Set α} (h : IsPreconnected s) : s.Subsingleton

instance Pi.totallyDisconnectedSpace {α : Type u_3} {β : α → Type u_4} [(a : α) → TopologicalSpace (β a)] [∀ (a : α), TotallyDisconnectedSpace (β a)] : TotallyDisconnectedSpace ((a : α) → β a)

Equations

• ⋯ = ⋯

instance Prod.totallyDisconnectedSpace {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [TotallyDisconnectedSpace α] [TotallyDisconnectedSpace β] : TotallyDisconnectedSpace (α × β)

Equations

• ⋯ = ⋯

instance instTotallyDisconnectedSpaceSum {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [TotallyDisconnectedSpace α] [TotallyDisconnectedSpace β] : TotallyDisconnectedSpace (α ⊕ β)

Equations

• ⋯ = ⋯

instance instTotallyDisconnectedSpaceSigma {ι : Type u_1} {π : ι → Type u_2} [(i : ι) → TopologicalSpace (π i)] [∀ (i : ι), TotallyDisconnectedSpace (π i)] : TotallyDisconnectedSpace ((i : ι) × π i)

Equations

• ⋯ = ⋯

theorem isTotallyDisconnected_of_isClopen_set {X : Type u_3} [TopologicalSpace X] (hX : Pairwise fun (x y : X) => ∃ (U : Set X), IsClopen U ∧ x ∈ U ∧ y ∉ U) : IsTotallyDisconnected Set.univ

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.

theorem totallyDisconnectedSpace_iff_connectedComponent_subsingleton {α : Type u} [TopologicalSpace α] : TotallyDisconnectedSpace α ↔ ∀ (x : α), (connectedComponent x).Subsingleton

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

theorem totallyDisconnectedSpace_iff_connectedComponent_singleton {α : Type u} [TopologicalSpace α] : TotallyDisconnectedSpace α ↔ ∀ (x : α), connectedComponent x = {x}

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

@[simp]

theorem connectedComponent_eq_singleton {α : Type u} [TopologicalSpace α] [TotallyDisconnectedSpace α] (x : α) : connectedComponent x = {x}

@[simp]

theorem Continuous.image_connectedComponent_eq_singleton {α : Type u} [TopologicalSpace α] {β : Type u_3} [TopologicalSpace β] [TotallyDisconnectedSpace β] {f : α → β} (h : Continuous f) (a : α) : f '' connectedComponent a = {f a}

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

theorem isTotallyDisconnected_of_totallyDisconnectedSpace {α : Type u} [TopologicalSpace α] [TotallyDisconnectedSpace α] (s : Set α) : IsTotallyDisconnected s

theorem isTotallyDisconnected_of_image {α : Type u} {β : Type v} [TopologicalSpace α] {s : Set α} [TopologicalSpace β] {f : α → β} (hf : ContinuousOn f s) (hf' : Function.Injective f) (h : IsTotallyDisconnected (f '' s)) : IsTotallyDisconnected s

theorem Embedding.isTotallyDisconnected {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} (hf : Embedding f) {s : Set α} (h : IsTotallyDisconnected (f '' s)) : IsTotallyDisconnected s

theorem Embedding.isTotallyDisconnected_image {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} (hf : Embedding f) {s : Set α} : IsTotallyDisconnected (f '' s) ↔ IsTotallyDisconnected s

theorem Embedding.isTotallyDisconnected_range {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} (hf : Embedding f) : IsTotallyDisconnected (Set.range f) ↔ TotallyDisconnectedSpace α

theorem totallyDisconnectedSpace_subtype_iff {α : Type u} [TopologicalSpace α] {s : Set α} : TotallyDisconnectedSpace ↑s ↔ IsTotallyDisconnected s

instance Subtype.totallyDisconnectedSpace {α : Type u_3} {p : α → Prop} [TopologicalSpace α] [TotallyDisconnectedSpace α] : TotallyDisconnectedSpace (Subtype p)

Equations

• ⋯ = ⋯

def IsTotallySeparated {α : Type u} [TopologicalSpace α] (s : Set α) : Prop

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

• IsTotallySeparated s = s.Pairwise fun (x y : α) => ∃ (u : Set α) (v : Set α), IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ s ⊆ u ∪ v ∧ Disjoint u v

theorem isTotallySeparated_empty {α : Type u} [TopologicalSpace α] : IsTotallySeparated ∅

theorem isTotallySeparated_singleton {α : Type u} [TopologicalSpace α] {x : α} : IsTotallySeparated {x}

theorem isTotallyDisconnected_of_isTotallySeparated {α : Type u} [TopologicalSpace α] {s : Set α} (H : IsTotallySeparated s) : IsTotallyDisconnected s

theorem IsTotallySeparated.isTotallyDisconnected {α : Type u} [TopologicalSpace α] {s : Set α} (H : IsTotallySeparated s) : IsTotallyDisconnected s

Alias of isTotallyDisconnected_of_isTotallySeparated.

class TotallySeparatedSpace (α : Type u) [TopologicalSpace α] : Prop

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.

theorem TotallySeparatedSpace.isTotallySeparated_univ {α : Type u} [TopologicalSpace α] [self : TotallySeparatedSpace α] : IsTotallySeparated Set.univ

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

@[instance 100]

instance TotallySeparatedSpace.totallyDisconnectedSpace (α : Type u) [TopologicalSpace α] [TotallySeparatedSpace α] : TotallyDisconnectedSpace α

Equations

• ⋯ = ⋯

@[instance 100]

instance TotallySeparatedSpace.of_discrete (α : Type u_3) [TopologicalSpace α] [DiscreteTopology α] : TotallySeparatedSpace α

Equations

• ⋯ = ⋯

theorem exists_isClopen_of_totally_separated {α : Type u_3} [TopologicalSpace α] [TotallySeparatedSpace α] {x : α} {y : α} (hxy : x ≠ y) : ∃ (U : Set α), IsClopen U ∧ x ∈ U ∧ y ∈ Uᶜ

theorem Continuous.image_eq_of_connectedComponent_eq {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [TotallyDisconnectedSpace β] {f : α → β} (h : Continuous f) (a : α) (b : α) (hab : connectedComponent a = connectedComponent b) : f a = f b

def Continuous.connectedComponentsLift {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [TotallyDisconnectedSpace β] {f : α → β} (h : Continuous f) : ConnectedComponents α → β

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

Equations

• h.connectedComponentsLift x = Quotient.liftOn' x f ⋯

theorem Continuous.connectedComponentsLift_continuous {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [TotallyDisconnectedSpace β] {f : α → β} (h : Continuous f) : Continuous h.connectedComponentsLift

@[simp]

theorem Continuous.connectedComponentsLift_apply_coe {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [TotallyDisconnectedSpace β] {f : α → β} (h : Continuous f) (x : α) : h.connectedComponentsLift (ConnectedComponents.mk x) = f x

@[simp]

theorem Continuous.connectedComponentsLift_comp_coe {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [TotallyDisconnectedSpace β] {f : α → β} (h : Continuous f) : h.connectedComponentsLift ∘ ConnectedComponents.mk = f

theorem connectedComponents_lift_unique' {α : Type u} [TopologicalSpace α] {β : Sort u_3} {g₁ : ConnectedComponents α → β} {g₂ : ConnectedComponents α → β} (hg : g₁ ∘ ConnectedComponents.mk = g₂ ∘ ConnectedComponents.mk) : g₁ = g₂

theorem Continuous.connectedComponentsLift_unique {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [TotallyDisconnectedSpace β] {f : α → β} (h : Continuous f) (g : ConnectedComponents α → β) (hg : g ∘ ConnectedComponents.mk = f) : g = h.connectedComponentsLift

instance ConnectedComponents.totallyDisconnectedSpace {α : Type u} [TopologicalSpace α] : TotallyDisconnectedSpace (ConnectedComponents α)

Equations

• ⋯ = ⋯

def Continuous.connectedComponentsMap {α : Type u} [TopologicalSpace α] {β : Type u_3} [TopologicalSpace β] {f : α → β} (h : Continuous f) : ConnectedComponents α → ConnectedComponents β

Functoriality of connectedComponents

Equations

• h.connectedComponentsMap = ⋯.connectedComponentsLift

theorem Continuous.connectedComponentsMap_continuous {α : Type u} [TopologicalSpace α] {β : Type u_3} [TopologicalSpace β] {f : α → β} (h : Continuous f) : Continuous h.connectedComponentsMap

theorem IsPreconnected.constant {α : Type u} [TopologicalSpace α] {Y : Type u_3} [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

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} [TopologicalSpace α] {Y : Type u_3} [TopologicalSpace Y] [DiscreteTopology Y] (hp : PreconnectedSpace α) {f : α → Y} (hf : Continuous f) {x : α} {y : α} : f x = f y

A PreconnectedSpace version of isPreconnected.constant

theorem IsPreconnected.constant_of_mapsTo {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] {S : Set α} (hS : IsPreconnected S) {T : Set β} [DiscreteTopology ↑T] {f : α → β} (hc : ContinuousOn f S) (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} [TopologicalSpace α] [TopologicalSpace β] {S : Set α} (hS : IsPreconnected S) {T : Set β} [DiscreteTopology ↑T] {f : α → β} (hc : ContinuousOn f S) (hTm : Set.MapsTo f S T) (hne : T.Nonempty) : ∃ y ∈ T, Set.EqOn f (Function.const α y) 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.