mathlib documentation

topology.connected

Connected subsets of topological spaces #

In this file we define connected subsets of a topological spaces and various other properties and classes related to connectivity.

Main definitions #

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

For each of these definitions, we also have a class stating that the whole space satisfies that property: connected_space, totally_disconnected_space, totally_separated_space.

On the definition of connected sets/spaces #

In informal mathematics, connected spaces are assumed to be nonempty. We formalise the predicate without that assumption as is_preconnected. In other words, the only difference is whether the empty space counts as connected. There are good reasons to consider the empty space to be “too simple to be simple” See also https://ncatlab.org/nlab/show/too+simple+to+be+simple, and in particular https://ncatlab.org/nlab/show/too+simple+to+be+simple#relationship_to_biased_definitions.

source
def is_preconnected {α : Type u} [topological_space α] (s : set α) :
Prop

A preconnected set is one where there is no non-trivial open partition.

Equations
source
def is_connected {α : Type u} [topological_space α] (s : set α) :
Prop

A connected set is one that is nonempty and where there is no non-trivial open partition.

Equations
source
theorem is_connected.nonempty {α : Type u} [topological_space α] {s : set α} (h : is_connected s) :
s.nonempty
source
theorem is_connected.is_preconnected {α : Type u} [topological_space α] {s : set α} (h : is_connected s) :
is_preconnected s
source
theorem is_preirreducible.is_preconnected {α : Type u} [topological_space α] {s : set α} (H : is_preirreducible s) :
is_preconnected s
source
theorem is_irreducible.is_connected {α : Type u} [topological_space α] {s : set α} (H : is_irreducible s) :
is_connected s
source
theorem is_preconnected_empty {α : Type u} [topological_space α] :
is_preconnected ∅
source
theorem is_connected_singleton {α : Type u} [topological_space α] {x : α} :
is_connected {x}
source
theorem is_preconnected_singleton {α : Type u} [topological_space α] {x : α} :
is_preconnected {x}
source
theorem set.subsingleton.is_preconnected {α : Type u} [topological_space α] {s : set α} (hs : s.subsingleton) :
is_preconnected s
source
theorem is_preconnected_of_forall {α : Type u} [topological_space α] {s : set α} (x : α) (H : ∀ (y : α), y ∈ s → (∃ (t : set α) (H : t ⊆ s), x ∈ t ∧ y ∈ t ∧ is_preconnected t)) :
is_preconnected s

If any point of a set is joined to a fixed point by a preconnected subset, then the original set is preconnected as well.

source
theorem is_preconnected_of_forall_pair {α : Type u} [topological_space α] {s : set α} (H : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → (∃ (t : set α) (H : t ⊆ s), x ∈ t ∧ y ∈ t ∧ is_preconnected t)) :
is_preconnected s

If any two points of a set are contained in a preconnected subset, then the original set is preconnected as well.

source
theorem is_preconnected_sUnion {α : Type u} [topological_space α] (x : α) (c : set (set α)) (H1 : ∀ (s : set α), s ∈ c → x ∈ s) (H2 : ∀ (s : set α), s ∈ c → is_preconnected s) :
is_preconnected (⋃₀c)

A union of a family of preconnected sets with a common point is preconnected as well.

source
theorem is_preconnected_Union {α : Type u} [topological_space α] {ι : Sort u_1} {s : ι → set α} (h₁ : (⋂ (i : ι), s i).nonempty) (h₂ : ∀ (i : ι), is_preconnected (s i)) :
is_preconnected (⋃ (i : ι), s i)
source
theorem is_preconnected.union {α : Type u} [topological_space α] (x : α) {s t : set α} (H1 : x ∈ s) (H2 : x ∈ t) (H3 : is_preconnected s) (H4 : is_preconnected t) :
is_preconnected (s ∪ t)
source
theorem is_preconnected.union' {α : Type u} [topological_space α] {s t : set α} (H : (s ∩ t).nonempty) (hs : is_preconnected s) (ht : is_preconnected t) :
is_preconnected (s ∪ t)
source
theorem is_connected.union {α : Type u} [topological_space α] {s t : set α} (H : (s ∩ t).nonempty) (Hs : is_connected s) (Ht : is_connected t) :
is_connected (s ∪ t)
source
theorem is_preconnected.sUnion_directed {α : Type u} [topological_space α] {S : set (set α)} (K : directed_on has_subset.subset S) (H : ∀ (s : set α), s ∈ S → is_preconnected s) :
is_preconnected (⋃₀S)

The directed sUnion of a set S of preconnected subsets is preconnected.

source
theorem is_preconnected.bUnion_of_refl_trans_gen {α : Type u} [topological_space α] {ι : Type u_1} {t : set ι} {s : ι → set α} (H : ∀ (i : ι), i ∈ t → is_preconnected (s i)) (K : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → relation.refl_trans_gen (λ (i j : ι), (s i ∩ s j).nonempty ∧ i ∈ t) i j) :
is_preconnected (⋃ (n : ι) (H : n ∈ t), s n)

The bUnion of a family of preconnected sets is preconnected if the graph determined by whether two sets intersect is preconnected.

source
theorem is_connected.bUnion_of_refl_trans_gen {α : Type u} [topological_space α] {ι : Type u_1} {t : set ι} {s : ι → set α} (ht : t.nonempty) (H : ∀ (i : ι), i ∈ t → is_connected (s i)) (K : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → relation.refl_trans_gen (λ (i j : ι), (s i ∩ s j).nonempty ∧ i ∈ t) i j) :
is_connected (⋃ (n : ι) (H : n ∈ t), s n)

The bUnion of a family of preconnected sets is preconnected if the graph determined by whether two sets intersect is preconnected.

source
theorem is_preconnected.Union_of_refl_trans_gen {α : Type u} [topological_space α] {ι : Type u_1} {s : ι → set α} (H : ∀ (i : ι), is_preconnected (s i)) (K : ∀ (i j : ι), relation.refl_trans_gen (λ (i j : ι), (s i ∩ s j).nonempty) i j) :
is_preconnected (⋃ (n : ι), s n)

Preconnectedness of the Union of a family of preconnected sets indexed by the vertices of a preconnected graph, where two vertices are joined when the corresponding sets intersect.

source
theorem is_connected.Union_of_refl_trans_gen {α : Type u} [topological_space α] {ι : Type u_1} [nonempty ι] {s : ι → set α} (H : ∀ (i : ι), is_connected (s i)) (K : ∀ (i j : ι), relation.refl_trans_gen (λ (i j : ι), (s i ∩ s j).nonempty) i j) :
is_connected (⋃ (n : ι), s n)
source
theorem is_preconnected.Union_of_chain {α : Type u} {β : Type v} [topological_space α] [linear_order β] [succ_order β] [is_succ_archimedean β] {s : β → set α} (H : ∀ (n : β), is_preconnected (s n)) (K : ∀ (n : β), (s n ∩ s (order.succ n)).nonempty) :
is_preconnected (⋃ (n : β), s n)

The Union of connected sets indexed by a type with an archimedean successor (like ℕ or ℤ) such that any two neighboring sets meet is preconnected.

source
theorem is_connected.Union_of_chain {α : Type u} {β : Type v} [topological_space α] [linear_order β] [succ_order β] [is_succ_archimedean β] [nonempty β] {s : β → set α} (H : ∀ (n : β), is_connected (s n)) (K : ∀ (n : β), (s n ∩ s (order.succ n)).nonempty) :
is_connected (⋃ (n : β), s n)

The Union of connected sets indexed by a type with an archimedean successor (like ℕ or ℤ) such that any two neighboring sets meet is connected.

source
theorem is_preconnected.bUnion_of_chain {α : Type u} {β : Type v} [topological_space α] [linear_order β] [succ_order β] [is_succ_archimedean β] {s : β → set α} {t : set β} (ht : t.ord_connected) (H : ∀ (n : β), n ∈ t → is_preconnected (s n)) (K : ∀ (n : β), n ∈ t → order.succ n ∈ t → (s n ∩ s (order.succ n)).nonempty) :
is_preconnected (⋃ (n : β) (H : n ∈ t), s n)

The Union of preconnected sets indexed by a subset of a type with an archimedean successor (like ℕ or ℤ) such that any two neighboring sets meet is preconnected.

source
theorem is_connected.bUnion_of_chain {α : Type u} {β : Type v} [topological_space α] [linear_order β] [succ_order β] [is_succ_archimedean β] {s : β → set α} {t : set β} (hnt : t.nonempty) (ht : t.ord_connected) (H : ∀ (n : β), n ∈ t → is_connected (s n)) (K : ∀ (n : β), n ∈ t → order.succ n ∈ t → (s n ∩ s (order.succ n)).nonempty) :
is_connected (⋃ (n : β) (H : n ∈ t), s n)

The Union of connected sets indexed by a subset of a type with an archimedean successor (like ℕ or ℤ) such that any two neighboring sets meet is preconnected.

source
theorem is_preconnected.subset_closure {α : Type u} [topological_space α] {s t : set α} (H : is_preconnected s) (Kst : s ⊆ t) (Ktcs : t ⊆ closure s) :
is_preconnected t

Theorem of bark and tree : if a set is within a (pre)connected set and its closure, then it is (pre)connected as well.

source
theorem is_connected.subset_closure {α : Type u} [topological_space α] {s t : set α} (H : is_connected s) (Kst : s ⊆ t) (Ktcs : t ⊆ closure s) :
is_connected t
source
theorem is_preconnected.closure {α : Type u} [topological_space α] {s : set α} (H : is_preconnected s) :
is_preconnected (closure s)

The closure of a (pre)connected set is (pre)connected as well.

source
theorem is_connected.closure {α : Type u} [topological_space α] {s : set α} (H : is_connected s) :
is_connected (closure s)
source
theorem is_preconnected.image {α : Type u} {β : Type v} [topological_space α] [topological_space β] {s : set α} (H : is_preconnected s) (f : α → β) (hf : continuous_on f s) :
is_preconnected (f '' s)

The image of a (pre)connected set is (pre)connected as well.

source
theorem is_connected.image {α : Type u} {β : Type v} [topological_space α] [topological_space β] {s : set α} (H : is_connected s) (f : α → β) (hf : continuous_on f s) :
is_connected (f '' s)
source
theorem is_preconnected_closed_iff {α : Type u} [topological_space α] {s : set α} :
is_preconnected s ↔ ∀ (t t' : set α), is_closed t → is_closed t' → s ⊆ t ∪ t' → (s ∩ t).nonempty → (s ∩ t').nonempty → (s ∩ (t ∩ t')).nonempty
source
theorem inducing.is_preconnected_image {α : Type u} {β : Type v} [topological_space α] [topological_space β] {s : set α} {f : α → β} (hf : inducing f) :
is_preconnected (f '' s) ↔ is_preconnected s
source
theorem is_preconnected.preimage_of_open_map {α : Type u} {β : Type v} [topological_space α] [topological_space β] {s : set β} (hs : is_preconnected s) {f : α → β} (hinj : function.injective f) (hf : is_open_map f) (hsf : s ⊆ set.range f) :
is_preconnected (f ⁻¹' s)
source
theorem is_preconnected.preimage_of_closed_map {α : Type u} {β : Type v} [topological_space α] [topological_space β] {s : set β} (hs : is_preconnected s) {f : α → β} (hinj : function.injective f) (hf : is_closed_map f) (hsf : s ⊆ set.range f) :
is_preconnected (f ⁻¹' s)
source
theorem is_connected.preimage_of_open_map {α : Type u} {β : Type v} [topological_space α] [topological_space β] {s : set β} (hs : is_connected s) {f : α → β} (hinj : function.injective f) (hf : is_open_map f) (hsf : s ⊆ set.range f) :
is_connected (f ⁻¹' s)
source
theorem is_connected.preimage_of_closed_map {α : Type u} {β : Type v} [topological_space α] [topological_space β] {s : set β} (hs : is_connected s) {f : α → β} (hinj : function.injective f) (hf : is_closed_map f) (hsf : s ⊆ set.range f) :
is_connected (f ⁻¹' s)
source
theorem is_preconnected.subset_or_subset {α : Type u} [topological_space α] {s u v : set α} (hu : is_open u) (hv : is_open v) (huv : disjoint u v) (hsuv : s ⊆ u ∪ v) (hs : is_preconnected s) :
s ⊆ u ∨ s ⊆ v
source
theorem is_preconnected.subset_left_of_subset_union {α : Type u} [topological_space α] {s u v : set α} (hu : is_open u) (hv : is_open v) (huv : disjoint u v) (hsuv : s ⊆ u ∪ v) (hsu : (s ∩ u).nonempty) (hs : is_preconnected s) :
s ⊆ u
source
theorem is_preconnected.subset_right_of_subset_union {α : Type u} [topological_space α] {s u v : set α} (hu : is_open u) (hv : is_open v) (huv : disjoint u v) (hsuv : s ⊆ u ∪ v) (hsv : (s ∩ v).nonempty) (hs : is_preconnected s) :
s ⊆ v
source
theorem is_preconnected.prod {α : Type u} {β : Type v} [topological_space α] [topological_space β] {s : set α} {t : set β} (hs : is_preconnected s) (ht : is_preconnected t) :
is_preconnected (s ×ˢ t)
source
theorem is_connected.prod {α : Type u} {β : Type v} [topological_space α] [topological_space β] {s : set α} {t : set β} (hs : is_connected s) (ht : is_connected t) :
is_connected (s ×ˢ t)
source
theorem is_preconnected_univ_pi {ι : Type u_1} {π : ι → Type u_2} [Π (i : ι), topological_space (π i)] {s : Π (i : ι), set (π i)} (hs : ∀ (i : ι), is_preconnected (s i)) :
is_preconnected (set.univ.pi s)
source
@[simp]
theorem is_connected_univ_pi {ι : Type u_1} {π : ι → Type u_2} [Π (i : ι), topological_space (π i)] {s : Π (i : ι), set (π i)} :
is_connected (set.univ.pi s) ↔ ∀ (i : ι), is_connected (s i)
source
theorem sigma.is_connected_iff {ι : Type u_1} {π : ι → Type u_2} [Π (i : ι), topological_space (π i)] {s : set (Σ (i : ι), π i)} :
is_connected s ↔ ∃ (i : ι) (t : set (π i)), is_connected t ∧ s = sigma.mk i '' t
source
theorem sigma.is_preconnected_iff {ι : Type u_1} {π : ι → Type u_2} [hι : nonempty ι] [Π (i : ι), topological_space (π i)] {s : set (Σ (i : ι), π i)} :
is_preconnected s ↔ ∃ (i : ι) (t : set (π i)), is_preconnected t ∧ s = sigma.mk i '' t
source
theorem sum.is_connected_iff {α : Type u} {β : Type v} [topological_space α] [topological_space β] {s : set (α ⊕ β)} :
is_connected s ↔ (∃ (t : set α), is_connected t ∧ s = sum.inl '' t) ∨ ∃ (t : set β), is_connected t ∧ s = sum.inr '' t
source
theorem sum.is_preconnected_iff {α : Type u} {β : Type v} [topological_space α] [topological_space β] {s : set (α ⊕ β)} :
is_preconnected s ↔ (∃ (t : set α), is_preconnected t ∧ s = sum.inl '' t) ∨ ∃ (t : set β), is_preconnected t ∧ s = sum.inr '' t
source
def connected_component {α : Type u} [topological_space α] (x : α) :
set α

The connected component of a point is the maximal connected set that contains this point.

Equations
source
def connected_component_in {α : Type u} [topological_space α] (F : set α) (x : ↥F) :
set α

The connected component of a point inside a set.

Equations
source
theorem mem_connected_component {α : Type u} [topological_space α] {x : α} :
x ∈ connected_component x
source
theorem is_preconnected_connected_component {α : Type u} [topological_space α] {x : α} :
is_preconnected (connected_component x)
source
theorem is_connected_connected_component {α : Type u} [topological_space α] {x : α} :
is_connected (connected_component x)
source
theorem is_preconnected.subset_connected_component {α : Type u} [topological_space α] {x : α} {s : set α} (H1 : is_preconnected s) (H2 : x ∈ s) :
s ⊆ connected_component x
source
theorem is_connected.subset_connected_component {α : Type u} [topological_space α] {x : α} {s : set α} (H1 : is_connected s) (H2 : x ∈ s) :
s ⊆ connected_component x
source
theorem connected_component_eq {α : Type u} [topological_space α] {x y : α} (h : y ∈ connected_component x) :
connected_component x = connected_component y
source
theorem connected_component_disjoint {α : Type u} [topological_space α] {x y : α} (h : connected_component x ≠ connected_component y) :
disjoint (connected_component x) (connected_component y)
source
theorem is_closed_connected_component {α : Type u} [topological_space α] {x : α} :
is_closed (connected_component x)
source
theorem continuous.image_connected_component_subset {α : Type u} {β : Type v} [topological_space α] [topological_space β] {f : α → β} (h : continuous f) (a : α) :
f '' connected_component a ⊆ connected_component (f a)
source
theorem continuous.maps_to_connected_component {α : Type u} {β : Type v} [topological_space α] [topological_space β] {f : α → β} (h : continuous f) (a : α) :
set.maps_to f (connected_component a) (connected_component (f a))
source
theorem irreducible_component_subset_connected_component {α : Type u} [topological_space α] {x : α} :
irreducible_component x ⊆ connected_component x
source
@[class]
structure preconnected_space (α : Type u) [topological_space α] :
Prop

A preconnected space is one where there is no non-trivial open partition.

Instances
source
@[class]
structure connected_space (α : Type u) [topological_space α] :
Prop

A connected space is a nonempty one where there is no non-trivial open partition.

Instances
source
theorem is_connected_univ {α : Type u} [topological_space α] [connected_space α] :
is_connected set.univ
source
theorem is_preconnected_range {α : Type u} {β : Type v} [topological_space α] [topological_space β] [preconnected_space α] {f : α → β} (h : continuous f) :
is_preconnected (set.range f)
source
theorem is_connected_range {α : Type u} {β : Type v} [topological_space α] [topological_space β] [connected_space α] {f : α → β} (h : continuous f) :
is_connected (set.range f)
source
theorem dense_range.preconnected_space {α : Type u} {β : Type v} [topological_space α] [topological_space β] [preconnected_space α] {f : α → β} (hf : dense_range f) (hc : continuous f) :
preconnected_space β
source
theorem connected_space_iff_connected_component {α : Type u} [topological_space α] :
connected_space α ↔ ∃ (x : α), connected_component x = set.univ
source
theorem preconnected_space_iff_connected_component {α : Type u} [topological_space α] :
preconnected_space α ↔ ∀ (x : α), connected_component x = set.univ
source
@[simp]
theorem preconnected_space.connected_component_eq_univ {X : Type u_1} [topological_space X] [h : preconnected_space X] (x : X) :
connected_component x = set.univ
source
@[protected, instance]
def prod.preconnected_space {α : Type u} {β : Type v} [topological_space α] [topological_space β] [preconnected_space α] [preconnected_space β] :
preconnected_space (α × β)
source
@[protected, instance]
def prod.connected_space {α : Type u} {β : Type v} [topological_space α] [topological_space β] [connected_space α] [connected_space β] :
connected_space (α × β)
source
@[protected, instance]
def pi.preconnected_space {ι : Type u_1} {π : ι → Type u_2} [Π (i : ι), topological_space (π i)] [∀ (i : ι), preconnected_space (π i)] :
preconnected_space (Π (i : ι), π i)
source
@[protected, instance]
def pi.connected_space {ι : Type u_1} {π : ι → Type u_2} [Π (i : ι), topological_space (π i)] [∀ (i : ι), connected_space (π i)] :
connected_space (Π (i : ι), π i)
source
@[protected, instance]
def preirreducible_space.preconnected_space (α : Type u) [topological_space α] [preirreducible_space α] :
preconnected_space α
source
@[protected, instance]
def irreducible_space.connected_space (α : Type u) [topological_space α] [irreducible_space α] :
connected_space α
source
theorem nonempty_inter {α : Type u} [topological_space α] [preconnected_space α] {s t : set α} :
is_open s → is_open t → s ∪ t = set.univ → s.nonempty → t.nonempty → (s ∩ t).nonempty
source
theorem is_clopen_iff {α : Type u} [topological_space α] [preconnected_space α] {s : set α} :
is_clopen s ↔ s = ∅ ∨ s = set.univ
source
theorem eq_univ_of_nonempty_clopen {α : Type u} [topological_space α] [preconnected_space α] {s : set α} (h : s.nonempty) (h' : is_clopen s) :
s = set.univ
source
theorem frontier_eq_empty_iff {α : Type u} [topological_space α] [preconnected_space α] {s : set α} :
frontier s = ∅ ↔ s = ∅ ∨ s = set.univ
source
theorem nonempty_frontier_iff {α : Type u} [topological_space α] [preconnected_space α] {s : set α} :
(frontier s).nonempty ↔ s.nonempty ∧ s ≠ set.univ
source
theorem subtype.preconnected_space {α : Type u} [topological_space α] {s : set α} (h : is_preconnected s) :
preconnected_space ↥s
source
theorem subtype.connected_space {α : Type u} [topological_space α] {s : set α} (h : is_connected s) :
connected_space ↥s
source
theorem is_preconnected_iff_preconnected_space {α : Type u} [topological_space α] {s : set α} :
is_preconnected s ↔ preconnected_space ↥s
source
theorem is_connected_iff_connected_space {α : Type u} [topological_space α] {s : set α} :
is_connected s ↔ connected_space ↥s
source
theorem is_preconnected_iff_subset_of_disjoint {α : Type u} [topological_space α] {s : set α} :
is_preconnected s ↔ ∀ (u v : set α), is_open u → is_open v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v

A set s is preconnected if and only if for every cover by two open sets that are disjoint on s, it is contained in one of the two covering sets.

source
theorem is_connected_iff_sUnion_disjoint_open {α : Type u} [topological_space α] {s : set α} :
is_connected s ↔ ∀ (U : finset (set α)), (∀ (u v : set α), u ∈ U → v ∈ U → (s ∩ (u ∩ v)).nonempty → u = v) → (∀ (u : set α), u ∈ U → is_open u) → s ⊆ ⋃₀↑U → (∃ (u : set α) (H : u ∈ U), s ⊆ u)

A set s is connected if and only if for every cover by a finite collection of open sets that are pairwise disjoint on s, it is contained in one of the members of the collection.

source
theorem is_preconnected.subset_clopen {α : Type u} [topological_space α] {s t : set α} (hs : is_preconnected s) (ht : is_clopen t) (hne : (s ∩ t).nonempty) :
s ⊆ t

Preconnected sets are either contained in or disjoint to any given clopen set.

source
theorem disjoint_or_subset_of_clopen {α : Type u} [topological_space α] {s t : set α} (hs : is_preconnected s) (ht : is_clopen t) :
disjoint s t ∨ s ⊆ t

Preconnected sets are either contained in or disjoint to any given clopen set.

source
theorem is_preconnected_iff_subset_of_disjoint_closed {α : Type u} [topological_space α] {s : set α} :
is_preconnected s ↔ ∀ (u v : set α), is_closed u → is_closed v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v

A set s is preconnected if and only if for every cover by two closed sets that are disjoint on s, it is contained in one of the two covering sets.

source
theorem is_preconnected_iff_subset_of_fully_disjoint_closed {α : Type u} [topological_space α] {s : set α} (hs : is_closed s) :
is_preconnected s ↔ ∀ (u v : set α), is_closed u → is_closed v → s ⊆ u ∪ v → u ∩ v = ∅ → s ⊆ u ∨ s ⊆ v

A closed set s is preconnected if and only if for every cover by two closed sets that are disjoint, it is contained in one of the two covering sets.

source
theorem is_clopen.connected_component_subset {α : Type u} [topological_space α] {s : set α} {x : α} (hs : is_clopen s) (hx : x ∈ s) :
connected_component x ⊆ s
source
theorem connected_component_subset_Inter_clopen {α : Type u} [topological_space α] {x : α} :
connected_component x ⊆ ⋂ (Z : {Z // is_clopen Z ∧ x ∈ Z}), ↑Z

The connected component of a point is always a subset of the intersection of all its clopen neighbourhoods.

source
theorem is_clopen.bUnion_connected_component_eq {α : Type u} [topological_space α] {Z : set α} (h : is_clopen Z) :
(⋃ (x : α) (H : x ∈ Z), connected_component x) = Z

A clopen set is the union of its connected components.

source
theorem preimage_connected_component_connected {α : Type u} {β : Type v} [topological_space α] [topological_space β] {f : α → β} (connected_fibers : ∀ (t : β), is_connected (f ⁻¹' {t})) (hcl : ∀ (T : set β), is_closed T ↔ is_closed (f ⁻¹' T)) (t : β) :
is_connected (f ⁻¹' connected_component t)

The preimage of a connected component is preconnected if the function has connected fibers and a subset is closed iff the preimage is.

source
theorem quotient_map.preimage_connected_component {α : Type u} {β : Type v} [topological_space α] [topological_space β] {f : α → β} (hf : quotient_map f) (h_fibers : ∀ (y : β), is_connected (f ⁻¹' {y})) (a : α) :
f ⁻¹' connected_component (f a) = connected_component a
source
theorem quotient_map.image_connected_component {α : Type u} {β : Type v} [topological_space α] [topological_space β] {f : α → β} (hf : quotient_map f) (h_fibers : ∀ (y : β), is_connected (f ⁻¹' {y})) (a : α) :
f '' connected_component a = connected_component (f a)
source
def is_totally_disconnected {α : Type u} [topological_space α] (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
source
theorem is_totally_disconnected_empty {α : Type u} [topological_space α] :
is_totally_disconnected ∅
source
theorem is_totally_disconnected_singleton {α : Type u} [topological_space α] {x : α} :
is_totally_disconnected {x}
source
@[class]
structure totally_disconnected_space (α : Type u) [topological_space α] :
Prop

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

Instances
source
theorem is_preconnected.subsingleton {α : Type u} [topological_space α] [totally_disconnected_space α] {s : set α} (h : is_preconnected s) :
s.subsingleton
source
@[protected, instance]
def pi.totally_disconnected_space {α : Type u_1} {β : α → Type u_2} [t₂ : Π (a : α), topological_space (β a)] [∀ (a : α), totally_disconnected_space (β a)] :
totally_disconnected_space (Π (a : α), β a)
source
@[protected, instance]
def prod.totally_disconnected_space {α : Type u} {β : Type v} [topological_space α] [topological_space β] [totally_disconnected_space α] [totally_disconnected_space β] :
totally_disconnected_space (α × β)
source
@[protected, instance]
def sum.totally_disconnected_space {α : Type u} {β : Type v} [topological_space α] [topological_space β] [totally_disconnected_space α] [totally_disconnected_space β] :
totally_disconnected_space (α ⊕ β)
source
@[protected, instance]
def sigma.totally_disconnected_space {ι : Type u_1} {π : ι → Type u_2} [Π (i : ι), topological_space (π i)] [∀ (i : ι), totally_disconnected_space (π i)] :
totally_disconnected_space (Σ (i : ι), π i)
source
theorem is_totally_disconnected_of_clopen_set {X : Type u_1} [topological_space X] (hX : ∀ {x y : X}, x ≠ y → (∃ (U : set X) (h_clopen : is_clopen U), x ∈ U ∧ y ∉ U)) :
is_totally_disconnected 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.

source
theorem totally_disconnected_space_iff_connected_component_subsingleton {α : Type u} [topological_space α] :
totally_disconnected_space α ↔ ∀ (x : α), (connected_component x).subsingleton

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

source
theorem totally_disconnected_space_iff_connected_component_singleton {α : Type u} [topological_space α] :
totally_disconnected_space α ↔ ∀ (x : α), connected_component x = {x}

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

source
@[simp]
theorem continuous.image_connected_component_eq_singleton {α : Type u} [topological_space α] {β : Type u_1} [topological_space β] [totally_disconnected_space β] {f : α → β} (h : continuous f) (a : α) :
f '' connected_component a = {f a}

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

source
theorem is_totally_disconnected_of_totally_disconnected_space {α : Type u} [topological_space α] [totally_disconnected_space α] (s : set α) :
is_totally_disconnected s
source
theorem is_totally_disconnected_of_image {α : Type u} {β : Type v} [topological_space α] {s : set α} [topological_space β] {f : α → β} (hf : continuous_on f s) (hf' : function.injective f) (h : is_totally_disconnected (f '' s)) :
is_totally_disconnected s
source
theorem embedding.is_totally_disconnected {α : Type u} {β : Type v} [topological_space α] [topological_space β] {f : α → β} (hf : embedding f) {s : set α} (h : is_totally_disconnected (f '' s)) :
is_totally_disconnected s
source
@[protected, instance]
def subtype.totally_disconnected_space {α : Type u_1} {p : α → Prop} [topological_space α] [totally_disconnected_space α] :
totally_disconnected_space (subtype p)
source
def is_totally_separated {α : Type u} [topological_space α] (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
source
theorem is_totally_separated_empty {α : Type u} [topological_space α] :
is_totally_separated ∅
source
theorem is_totally_separated_singleton {α : Type u} [topological_space α] {x : α} :
is_totally_separated {x}
source
theorem is_totally_disconnected_of_is_totally_separated {α : Type u} [topological_space α] {s : set α} (H : is_totally_separated s) :
is_totally_disconnected s
source
theorem is_totally_separated.is_totally_disconnected {α : Type u} [topological_space α] {s : set α} (H : is_totally_separated s) :
is_totally_disconnected s

Alias of is_totally_disconnected_of_is_totally_separated.

source
@[class]
structure totally_separated_space (α : Type u) [topological_space α] :
Prop

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

Instances
source
@[protected, instance]
def totally_separated_space.totally_disconnected_space (α : Type u) [topological_space α] [totally_separated_space α] :
totally_disconnected_space α
source
@[protected, instance]
def totally_separated_space.of_discrete (α : Type u_1) [topological_space α] [discrete_topology α] :
totally_separated_space α
source
theorem exists_clopen_of_totally_separated {α : Type u_1} [topological_space α] [totally_separated_space α] {x y : α} (hxy : x ≠ y) :
∃ (U : set α) (hU : is_clopen U), x ∈ U ∧ y ∈ Uᶜ
source
def connected_component_setoid (α : Type u_1) [topological_space α] :
setoid α

The setoid of connected components of a topological space

Equations
source
def connected_components (α : Type u) [topological_space α] :
Type u

The quotient of a space by its connected components

Equations
source
@[protected, instance]
def connected_components.has_coe_t {α : Type u} [topological_space α] :
has_coe_t α (connected_components α)
Equations
source
@[simp]
theorem connected_components.coe_eq_coe {α : Type u} [topological_space α] {x y : α} :
↑x = ↑y ↔ connected_component x = connected_component y
source
theorem connected_components.coe_ne_coe {α : Type u} [topological_space α] {x y : α} :
↑x ≠ ↑y ↔ connected_component x ≠ connected_component y
source
theorem connected_components.coe_eq_coe' {α : Type u} [topological_space α] {x y : α} :
↑x = ↑y ↔ x ∈ connected_component y
source
@[protected, instance]
def connected_components.inhabited {α : Type u} [topological_space α] [inhabited α] :
inhabited (connected_components α)
Equations
source
@[protected, instance]
def connected_components.topological_space {α : Type u} [topological_space α] :
topological_space (connected_components α)
Equations
source
theorem connected_components.surjective_coe {α : Type u} [topological_space α] :
function.surjective coe
source
theorem connected_components.quotient_map_coe {α : Type u} [topological_space α] :
quotient_map coe
source
@[continuity]
theorem connected_components.continuous_coe {α : Type u} [topological_space α] :
continuous coe
source
@[simp]
theorem connected_components.range_coe {α : Type u} [topological_space α] :
set.range coe = set.univ
source
theorem continuous.image_eq_of_connected_component_eq {α : Type u} {β : Type v} [topological_space α] [topological_space β] [totally_disconnected_space β] {f : α → β} (h : continuous f) (a b : α) (hab : connected_component a = connected_component b) :
f a = f b
source
def continuous.connected_components_lift {α : Type u} {β : Type v} [topological_space α] [topological_space β] [totally_disconnected_space β] {f : α → β} (h : continuous f) :
connected_components α → β

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

Equations
source
@[continuity]
theorem continuous.connected_components_lift_continuous {α : Type u} {β : Type v} [topological_space α] [topological_space β] [totally_disconnected_space β] {f : α → β} (h : continuous f) :
continuous h.connected_components_lift
source
@[simp]
theorem continuous.connected_components_lift_apply_coe {α : Type u} {β : Type v} [topological_space α] [topological_space β] [totally_disconnected_space β] {f : α → β} (h : continuous f) (x : α) :
h.connected_components_lift ↑x = f x
source
@[simp]
theorem continuous.connected_components_lift_comp_coe {α : Type u} {β : Type v} [topological_space α] [topological_space β] [totally_disconnected_space β] {f : α → β} (h : continuous f) :
h.connected_components_lift ∘ coe = f
source
theorem connected_components_lift_unique' {α : Type u} [topological_space α] {β : Sort u_1} {g₁ g₂ : connected_components α → β} (hg : g₁ ∘ coe = g₂ ∘ coe) :
g₁ = g₂
source
theorem continuous.connected_components_lift_unique {α : Type u} {β : Type v} [topological_space α] [topological_space β] [totally_disconnected_space β] {f : α → β} (h : continuous f) (g : connected_components α → β) (hg : g ∘ coe = f) :
g = h.connected_components_lift
source
theorem connected_components_preimage_singleton {α : Type u} [topological_space α] {x : α} :
coe ⁻¹' {↑x} = connected_component x

The preimage of a singleton in connected_components is the connected component of an element in the equivalence class.

source
theorem connected_components_preimage_image {α : Type u} [topological_space α] (U : set α) :
coe ⁻¹' (coe '' U) = ⋃ (x : α) (H : x ∈ U), connected_component x

The preimage of the image of a set under the quotient map to connected_components α is the union of the connected components of the elements in it.

source
@[protected, instance]
def connected_components.totally_disconnected_space {α : Type u} [topological_space α] :
totally_disconnected_space (connected_components α)
source
def continuous.connected_components_map {α : Type u} [topological_space α] {β : Type u_1} [topological_space β] {f : α → β} (h : continuous f) :
connected_components α → connected_components β

Functoriality of connected_components

Equations
source
theorem continuous.connected_components_map_continuous {α : Type u} [topological_space α] {β : Type u_1} [topological_space β] {f : α → β} (h : continuous f) :
continuous h.connected_components_map