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.

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

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

Equations
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
theorem is_connected.nonempty {α : Type u} [topological_space α] {s : set α} (h : is_connected s) :
theorem is_connected.is_preconnected {α : Type u} [topological_space α] {s : set α} (h : is_connected s) :
theorem is_irreducible.is_connected {α : Type u} [topological_space α] {s : set α} (H : is_irreducible s) :
theorem is_connected_singleton {α : Type u} [topological_space α] {x : α} :
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)) :

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

theorem is_preconnected_of_forall_pair {α : Type u} [topological_space α] {s : set α} (H : ∀ (x y : α), x sy s(∃ (t : set α) (H : t s), x t y t is_preconnected t)) :

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

theorem is_preconnected_sUnion {α : Type u} [topological_space α] (x : α) (c : set (set α)) (H1 : ∀ (s : set α), s cx s) (H2 : ∀ (s : set α), s cis_preconnected s) :

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

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) :
theorem is_connected.union {α : Type u} [topological_space α] {s t : set α} (H : (s t).nonempty) (Hs : is_connected s) (Ht : is_connected t) :
theorem is_preconnected.closure {α : Type u} [topological_space α] {s : set α} (H : is_preconnected s) :
theorem is_connected.closure {α : Type u} [topological_space α] {s : set α} (H : is_connected s) :
theorem is_preconnected.image {α : Type u} {β : Type v} [topological_space α] [topological_space β] {s : set α} (H : is_preconnected s) (f : α → β) (hf : continuous_on f s) :
theorem is_connected.image {α : Type u} {β : Type v} [topological_space α] [topological_space β] {s : set α} (H : is_connected s) (f : α → β) (hf : continuous_on f s) :
theorem is_preconnected_closed_iff {α : Type u} [topological_space α] {s : set α} :
is_preconnected s ∀ (t t' : set α), is_closed tis_closed t's t t'(s t).nonempty(s t').nonempty(s (t t')).nonempty
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
def connected_component_in {α : Type u} [topological_space α] (F : set α) (x : F) :
set α

The connected component of a point inside a set.

Equations
theorem mem_connected_component {α : Type u} [topological_space α] {x : α} :
theorem is_preconnected.subset_connected_component {α : Type u} [topological_space α] {x : α} {s : set α} (H1 : is_preconnected s) (H2 : x s) :
theorem is_connected.subset_connected_component {α : Type u} [topological_space α] {x : α} {s : set α} (H1 : is_connected s) (H2 : x s) :
theorem continuous.image_connected_component_subset {α : Type u} [topological_space α] {β : Type u_1} [topological_space β] {f : α → β} (h : continuous f) (a : α) :
@[class]
structure preconnected_space (α : Type u) [topological_space α] :
Prop

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

Instances
@[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
theorem is_connected_range {α : Type u} {β : Type v} [topological_space α] [topological_space β] [connected_space α] {f : α → β} (h : continuous f) :
theorem nonempty_inter {α : Type u} [topological_space α] [preconnected_space α] {s t : set α} :
is_open sis_open ts t = set.univs.nonemptyt.nonempty(s t).nonempty
theorem is_clopen_iff {α : Type u} [topological_space α] [preconnected_space α] {s : set α} :
theorem eq_univ_of_nonempty_clopen {α : Type u} [topological_space α] [preconnected_space α] {s : set α} (h : s.nonempty) (h' : is_clopen s) :
theorem subtype.connected_space {α : Type u} [topological_space α] {s : set α} (h : is_connected s) :
theorem is_preconnected_iff_subset_of_disjoint {α : Type u} [topological_space α] {s : set α} :
is_preconnected s ∀ (u v : set α), is_open uis_open vs u vs (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.

theorem is_connected_iff_sUnion_disjoint_open {α : Type u} [topological_space α] {s : set α} :
is_connected s ∀ (U : finset (set α)), (∀ (u v : set α), u Uv U(s (u v)).nonemptyu = v)(∀ (u : set α), u Uis_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.

theorem subset_or_disjoint_of_clopen {α : Type u_1} [topological_space α] {s t : set α} (h : is_preconnected t) (h1 : is_clopen s) :
s t = t s

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

theorem is_preconnected_iff_subset_of_disjoint_closed {α : Type u_1} {s : set α} [topological_space α] :
is_preconnected s ∀ (u v : set α), is_closed uis_closed vs u vs (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.

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 uis_closed vs u vu 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.

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.

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

A clopen set is the union of its connected components.

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

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

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
@[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)

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

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

@[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 : α) :

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

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)) :
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)) :
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
@[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
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
def connected_component_setoid (α : Type u_1) [topological_space α] :

The setoid of connected components of a topological space

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

The quotient of a space by its connected components

Equations
theorem continuous.image_eq_of_equiv {α : Type u} [topological_space α] {β : Type u_1} [topological_space β] [totally_disconnected_space β] {f : α → β} (h : continuous f) (a b : α) (hab : a b) :
f a = f b
def continuous.connected_components_lift {α : Type u} [topological_space α] {β : Type u_1} [topological_space β] [totally_disconnected_space β] {f : α → β} (h : continuous f) :

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

Equations
theorem continuous.connected_components_lift_unique {α : Type u} [topological_space α] {β : Type u_1} [topological_space β] [totally_disconnected_space β] {f : α → β} (h : continuous f) (g : connected_components α → β) (hg : g quotient.mk = f) :
theorem connected_components_lift_unique' {α : Type u} [topological_space α] {β : Type u_1} (g₁ g₂ : connected_components α → β) (hg : g₁ quotient.mk = g₂ quotient.mk) :
g₁ = g₂

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

theorem connected_components_preimage_image {α : Type u} [topological_space α] (U : set α) :
quotient.mk ⁻¹' (quotient.mk '' 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.