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

source
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, i.e. either empty or a singleton.

Equations

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

Instances For

source
theorem isTotallyDisconnected_empty {α : Type u} [TopologicalSpace α] :
IsTotallyDisconnected ∅
source
theorem isTotallyDisconnected_singleton {α : Type u} [TopologicalSpace α] {x : α} :
IsTotallyDisconnected {x}
source
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.

Instances

source
theorem totallyDisconnectedSpace_iff (α : Type u) [TopologicalSpace α] :
TotallyDisconnectedSpace α ↔ IsTotallyDisconnected Set.univ
source
theorem IsPreconnected.subsingleton {α : Type u} [TopologicalSpace α] [TotallyDisconnectedSpace α] {s : Set α} (h : IsPreconnected s) :
s.Subsingleton
source
instance Pi.totallyDisconnectedSpace {α : Type u_3} {β : α → Type u_4} [(a : α) → TopologicalSpace (β a)] [∀ (a : α), TotallyDisconnectedSpace (β a)] :
TotallyDisconnectedSpace ((a : α) → β a)
source
instance Prod.totallyDisconnectedSpace {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [TotallyDisconnectedSpace α] [TotallyDisconnectedSpace β] :
TotallyDisconnectedSpace (α × β)
source
instance instTotallyDisconnectedSpaceSum {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [TotallyDisconnectedSpace α] [TotallyDisconnectedSpace β] :
TotallyDisconnectedSpace (α ⊕ β)
source
instance instTotallyDisconnectedSpaceSigma {ι : Type u_1} {X : ι → Type u_2} [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), TotallyDisconnectedSpace (X i)] :
TotallyDisconnectedSpace ((i : ι) × X i)
source
theorem totallyDisconnectedSpace_iff_connectedComponent_subsingleton {α : Type u} [TopologicalSpace α] :
TotallyDisconnectedSpace α ↔ ∀ (x : α), (connectedComponent x).Subsingleton

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

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

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

source
@[simp]
theorem connectedComponent_eq_singleton {α : Type u} [TopologicalSpace α] [TotallyDisconnectedSpace α] (x : α) :
connectedComponent x = {x}
source
@[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.

source
theorem isTotallyDisconnected_of_totallyDisconnectedSpace {α : Type u} [TopologicalSpace α] [TotallyDisconnectedSpace α] (s : Set α) :
IsTotallyDisconnected s
source
theorem TotallyDisconnectedSpace.eq_of_continuous {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [PreconnectedSpace α] [TotallyDisconnectedSpace β] (f : α → β) (hf : Continuous f) (i j : α) :
f i = f j
source
noncomputable def TotallyDisconnectedSpace.continuousMapEquivOfConnectedSpace (X : Type u_3) (Y : Type u_4) [TopologicalSpace X] [TopologicalSpace Y] [TotallyDisconnectedSpace Y] [ConnectedSpace X] :
C(X, Y) ≃ Y

The bijection `C(X, Y) ≃ Y` when `Y` is totally disconnected and `X` is connected.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[simp]
theorem TotallyDisconnectedSpace.continuousMapEquivOfConnectedSpace_symm_apply_apply (X : Type u_3) (Y : Type u_4) [TopologicalSpace X] [TopologicalSpace Y] [TotallyDisconnectedSpace Y] [ConnectedSpace X] (y : Y) (x✝ : X) :
((continuousMapEquivOfConnectedSpace X Y).symm y) x✝ = y
source
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
source
theorem Topology.IsEmbedding.isTotallyDisconnected {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s : Set α} (hf : IsEmbedding f) (h : IsTotallyDisconnected (f '' s)) :
IsTotallyDisconnected s
source
theorem Topology.IsEmbedding.isTotallyDisconnected_image {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s : Set α} (hf : IsEmbedding f) :
IsTotallyDisconnected (f '' s) ↔ IsTotallyDisconnected s
source
theorem Topology.IsEmbedding.isTotallyDisconnected_range {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} (hf : IsEmbedding f) :
IsTotallyDisconnected (Set.range f) ↔ TotallyDisconnectedSpace α
source
theorem totallyDisconnectedSpace_subtype_iff {α : Type u} [TopologicalSpace α] {s : Set α} :
TotallyDisconnectedSpace ↑s ↔ IsTotallyDisconnected s
source
instance Subtype.totallyDisconnectedSpace {α : Type u_3} {p : α → Prop} [TopologicalSpace α] [TotallyDisconnectedSpace α] :
TotallyDisconnectedSpace (Subtype p)
source
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

Instances For

source
theorem isTotallySeparated_empty {α : Type u} [TopologicalSpace α] :
IsTotallySeparated ∅
source
theorem isTotallySeparated_singleton {α : Type u} [TopologicalSpace α] {x : α} :
IsTotallySeparated {x}
source
theorem isTotallyDisconnected_of_isTotallySeparated {α : Type u} [TopologicalSpace α] {s : Set α} (H : IsTotallySeparated s) :
IsTotallyDisconnected s
source
theorem IsTotallySeparated.isTotallyDisconnected {α : Type u} [TopologicalSpace α] {s : Set α} (H : IsTotallySeparated s) :
IsTotallyDisconnected s

Alias of `isTotallyDisconnected_of_isTotallySeparated`.

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

Instances

source
theorem totallySeparatedSpace_iff (α : Type u) [TopologicalSpace α] :
TotallySeparatedSpace α ↔ IsTotallySeparated Set.univ
source
@[instance 100]
instance TotallySeparatedSpace.totallyDisconnectedSpace (α : Type u) [TopologicalSpace α] [TotallySeparatedSpace α] :
TotallyDisconnectedSpace α
source
@[instance 100]
instance TotallySeparatedSpace.of_discrete (α : Type u_3) [TopologicalSpace α] [DiscreteTopology α] :
TotallySeparatedSpace α
source
theorem totallySeparatedSpace_iff_exists_isClopen {α : Type u_3} [TopologicalSpace α] :
TotallySeparatedSpace α ↔ Pairwise fun (x1 x2 : α) => ∃ (U : Set α), IsClopen U ∧ x1 ∈ U ∧ x2 ∈ U ᶜ
source
theorem exists_isClopen_of_totally_separated {α : Type u_3} [TopologicalSpace α] [TotallySeparatedSpace α] :
Pairwise fun (x1 x2 : α) => ∃ (U : Set α), IsClopen U ∧ x1 ∈ U ∧ x2 ∈ U ᶜ
source
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
source
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 ⋯

Instances For

source
theorem Continuous.connectedComponentsLift_continuous {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [TotallyDisconnectedSpace β] {f : α → β} (h : Continuous f) :
Continuous h.connectedComponentsLift
source
@[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
source
@[simp]
theorem Continuous.connectedComponentsLift_comp_coe {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [TotallyDisconnectedSpace β] {f : α → β} (h : Continuous f) :
h.connectedComponentsLift ∘ ConnectedComponents.mk = f
source
theorem connectedComponents_lift_unique' {α : Type u} [TopologicalSpace α] {β : Sort u_3} {g₁ g₂ : ConnectedComponents α → β} (hg : g₁ ∘ ConnectedComponents.mk = g₂ ∘ ConnectedComponents.mk) :
g₁ = g₂
source
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
source
instance ConnectedComponents.totallyDisconnectedSpace {α : Type u} [TopologicalSpace α] :
TotallyDisconnectedSpace (ConnectedComponents α)
source
def Continuous.connectedComponentsMap {α : Type u} [TopologicalSpace α] {β : Type u_3} [TopologicalSpace β] {f : α → β} (h : Continuous f) :
ConnectedComponents α → ConnectedComponents β

Functoriality of `connectedComponents`

Equations

- h.connectedComponentsMap = ⋯.connectedComponentsLift

Instances For

source
theorem Continuous.connectedComponentsMap_continuous {α : Type u} [TopologicalSpace α] {β : Type u_3} [TopologicalSpace β] {f : α → β} (h : Continuous f) :
Continuous h.connectedComponentsMap
source
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`

source
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`

source
theorem IsPreconnected.constant_of_mapsTo {α : Type u} [TopologicalSpace α] {S : Set α} (hS : IsPreconnected S) {β : Type u_3} [TopologicalSpace β] {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.

source
theorem IsPreconnected.eqOn_const_of_mapsTo {α : Type u} [TopologicalSpace α] {S : Set α} (hS : IsPreconnected S) {β : Type u_3} [TopologicalSpace β] {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`.