# mathlib3documentation

topology.connected

# Connected subsets of topological spaces #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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:

• `is_connected`: a nonempty set that has no non-trivial open partition. See also the section below in the module doc.
• `connected_component` is the connected component of an element in the space.
• `is_totally_disconnected`: all of its connected components are singletons.
• `is_totally_separated`: any two points can be separated by two disjoint opens that cover the set.

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} (s : set α) :
Prop

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

Equations
def is_connected {α : Type u} (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} {s : set α} (h : is_connected s) :
theorem is_connected.is_preconnected {α : Type u} {s : set α} (h : is_connected s) :
theorem is_preirreducible.is_preconnected {α : Type u} {s : set α} (H : is_preirreducible s) :
theorem is_irreducible.is_connected {α : Type u} {s : set α} (H : is_irreducible s) :
theorem is_preconnected_empty {α : Type u}  :
theorem is_connected_singleton {α : Type u} {x : α} :
theorem is_preconnected_singleton {α : Type u} {x : α} :
theorem set.subsingleton.is_preconnected {α : Type u} {s : set α} (hs : s.subsingleton) :
theorem is_preconnected_of_forall {α : Type u} {s : set α} (x : α) (H : (y : α), y s ( (t : set α) (H : t s), x t y 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} {s : set α} (H : (x : α), x s (y : α), y s ( (t : set α) (H : t s), x t y 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} (x : α) (c : set (set α)) (H1 : (s : set α), s c x s) (H2 : (s : set α), s c ) :

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

theorem is_preconnected_Union {α : Type u} {ι : Sort u_1} {s : ι set α} (h₁ : ( (i : ι), s i).nonempty) (h₂ : (i : ι), is_preconnected (s i)) :
is_preconnected ( (i : ι), s i)
theorem is_preconnected.union {α : Type u} (x : α) {s t : set α} (H1 : x s) (H2 : x t) (H3 : is_preconnected s) (H4 : is_preconnected t) :
theorem is_preconnected.union' {α : Type u} {s t : set α} (H : (s t).nonempty) (hs : is_preconnected s) (ht : is_preconnected t) :
theorem is_connected.union {α : Type u} {s t : set α} (H : (s t).nonempty) (Hs : is_connected s) (Ht : is_connected t) :
theorem is_preconnected.sUnion_directed {α : Type u} {S : set (set α)} (K : S) (H : (s : set α), s S ) :

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

theorem is_preconnected.bUnion_of_refl_trans_gen {α : Type u} {ι : 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.

theorem is_connected.bUnion_of_refl_trans_gen {α : Type u} {ι : 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.

theorem is_preconnected.Union_of_refl_trans_gen {α : Type u} {ι : 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.

theorem is_connected.Union_of_refl_trans_gen {α : Type u} {ι : 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)
theorem is_preconnected.Union_of_chain {α : Type u} {β : Type v} [linear_order β] [succ_order β] {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.

theorem is_connected.Union_of_chain {α : Type u} {β : Type v} [linear_order β] [succ_order β] [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.

theorem is_preconnected.bUnion_of_chain {α : Type u} {β : Type v} [linear_order β] [succ_order β] {s : β set α} {t : set β} (ht : t.ord_connected) (H : (n : β), n t is_preconnected (s n)) (K : (n : β), n t 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.

theorem is_connected.bUnion_of_chain {α : Type u} {β : Type v} [linear_order β] [succ_order β] {s : β set α} {t : set β} (hnt : t.nonempty) (ht : t.ord_connected) (H : (n : β), n t is_connected (s n)) (K : (n : β), n t 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.

theorem is_preconnected.subset_closure {α : Type u} {s t : set α} (H : is_preconnected s) (Kst : s t) (Ktcs : 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.

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

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

theorem is_connected.closure {α : Type u} {s : set α} (H : is_connected s) :
theorem is_preconnected.image {α : Type u} {β : Type v} {s : set α} (H : is_preconnected s) (f : α β) (hf : s) :

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

theorem is_connected.image {α : Type u} {β : Type v} {s : set α} (H : is_connected s) (f : α β) (hf : s) :
theorem is_preconnected_closed_iff {α : Type u} {s : set α} :
(t t' : set α), s t t' (s t).nonempty (s t').nonempty (s (t t')).nonempty
theorem inducing.is_preconnected_image {α : Type u} {β : Type v} {s : set α} {f : α β} (hf : inducing f) :
theorem is_preconnected.preimage_of_open_map {α : Type u} {β : Type v} {s : set β} (hs : is_preconnected s) {f : α β} (hinj : function.injective f) (hf : is_open_map f) (hsf : s ) :
theorem is_preconnected.preimage_of_closed_map {α : Type u} {β : Type v} {s : set β} (hs : is_preconnected s) {f : α β} (hinj : function.injective f) (hf : is_closed_map f) (hsf : s ) :
theorem is_connected.preimage_of_open_map {α : Type u} {β : Type v} {s : set β} (hs : is_connected s) {f : α β} (hinj : function.injective f) (hf : is_open_map f) (hsf : s ) :
theorem is_connected.preimage_of_closed_map {α : Type u} {β : Type v} {s : set β} (hs : is_connected s) {f : α β} (hinj : function.injective f) (hf : is_closed_map f) (hsf : s ) :
theorem is_preconnected.subset_or_subset {α : Type u} {s u v : set α} (hu : is_open u) (hv : is_open v) (huv : v) (hsuv : s u v) (hs : is_preconnected s) :
s u s v
theorem is_preconnected.subset_left_of_subset_union {α : Type u} {s u v : set α} (hu : is_open u) (hv : is_open v) (huv : v) (hsuv : s u v) (hsu : (s u).nonempty) (hs : is_preconnected s) :
s u
theorem is_preconnected.subset_right_of_subset_union {α : Type u} {s u v : set α} (hu : is_open u) (hv : is_open v) (huv : v) (hsuv : s u v) (hsv : (s v).nonempty) (hs : is_preconnected s) :
s v
theorem is_preconnected.subset_of_closure_inter_subset {α : Type u} {s u : set α} (hs : is_preconnected s) (hu : is_open u) (h'u : (s u).nonempty) (h : s u) :
s u

If a preconnected set `s` intersects an open set `u`, and limit points of `u` inside `s` are contained in `u`, then the whole set `s` is contained in `u`.

theorem is_preconnected.prod {α : Type u} {β : Type v} {s : set α} {t : set β} (hs : is_preconnected s) (ht : is_preconnected t) :
theorem is_connected.prod {α : Type u} {β : Type v} {s : set α} {t : set β} (hs : is_connected s) (ht : is_connected t) :
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)) :
@[simp]
theorem is_connected_univ_pi {ι : Type u_1} {π : ι Type u_2} [Π (i : ι), topological_space (π i)] {s : Π (i : ι), set (π i)} :
(i : ι), is_connected (s i)
theorem sigma.is_connected_iff {ι : Type u_1} {π : ι Type u_2} [Π (i : ι), topological_space (π i)] {s : set (Σ (i : ι), π i)} :
(i : ι) (t : set (π i)), s = '' t
theorem sigma.is_preconnected_iff {ι : Type u_1} {π : ι Type u_2} [hι : nonempty ι] [Π (i : ι), topological_space (π i)] {s : set (Σ (i : ι), π i)} :
(i : ι) (t : set (π i)), s = '' t
theorem sum.is_connected_iff {α : Type u} {β : Type v} {s : set β)} :
( (t : set α), s = (t : set β), s =
theorem sum.is_preconnected_iff {α : Type u} {β : Type v} {s : set β)} :
( (t : set α), s = (t : set β), s =
def connected_component {α : Type u} (x : α) :
set α

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

Equations
def connected_component_in {α : Type u} (F : set α) (x : α) :
set α

Given a set `F` in a topological space `α` and a point `x : α`, the connected component of `x` in `F` is the connected component of `x` in the subtype `F` seen as a set in `α`. This definition does not make sense if `x` is not in `F` so we return the empty set in this case.

Equations
theorem connected_component_in_eq_image {α : Type u} {F : set α} {x : α} (h : x F) :
=
theorem connected_component_in_eq_empty {α : Type u} {F : set α} {x : α} (h : x F) :
theorem mem_connected_component {α : Type u} {x : α} :
theorem mem_connected_component_in {α : Type u} {x : α} {F : set α} (hx : x F) :
theorem connected_component_nonempty {α : Type u} {x : α} :
theorem connected_component_in_nonempty_iff {α : Type u} {x : α} {F : set α} :
x F
theorem connected_component_in_subset {α : Type u} (F : set α) (x : α) :
theorem is_preconnected_connected_component {α : Type u} {x : α} :
theorem is_preconnected_connected_component_in {α : Type u} {x : α} {F : set α} :
theorem is_connected_connected_component {α : Type u} {x : α} :
theorem is_connected_connected_component_in_iff {α : Type u} {x : α} {F : set α} :
x F
theorem is_preconnected.subset_connected_component {α : Type u} {x : α} {s : set α} (H1 : is_preconnected s) (H2 : x s) :
theorem is_preconnected.subset_connected_component_in {α : Type u} {s : set α} {x : α} {F : set α} (hs : is_preconnected s) (hxs : x s) (hsF : s F) :
theorem is_connected.subset_connected_component {α : Type u} {x : α} {s : set α} (H1 : is_connected s) (H2 : x s) :
theorem is_preconnected.connected_component_in {α : Type u} {x : α} {F : set α} (h : is_preconnected F) (hx : x F) :
theorem connected_component_eq {α : Type u} {x y : α} (h : y ) :
theorem connected_component_eq_iff_mem {α : Type u} {x y : α} :
theorem connected_component_in_eq {α : Type u} {x y : α} {F : set α} (h : y ) :
theorem connected_component_in_univ {α : Type u} (x : α) :
theorem connected_component_disjoint {α : Type u} {x y : α}  :
theorem is_closed_connected_component {α : Type u} {x : α} :
theorem continuous.image_connected_component_subset {α : Type u} {β : Type v} {f : α β} (h : continuous f) (a : α) :
theorem continuous.maps_to_connected_component {α : Type u} {β : Type v} {f : α β} (h : continuous f) (a : α) :
theorem connected_component_in_mono {α : Type u} (x : α) {F G : set α} (h : F G) :
@[class]
structure preconnected_space (α : Type u)  :
Prop
• is_preconnected_univ :

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

Instances of this typeclass
@[class]
structure connected_space (α : Type u)  :
Prop
• to_preconnected_space :
• to_nonempty :

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

Instances of this typeclass
theorem is_connected_univ {α : Type u}  :
theorem is_preconnected_range {α : Type u} {β : Type v} {f : α β} (h : continuous f) :
theorem is_connected_range {α : Type u} {β : Type v} {f : α β} (h : continuous f) :
theorem dense_range.preconnected_space {α : Type u} {β : Type v} {f : α β} (hf : dense_range f) (hc : continuous f) :
@[simp]
@[protected, instance]
def prod.preconnected_space {α : Type u} {β : Type v}  :
@[protected, instance]
def prod.connected_space {α : Type u} {β : Type v}  :
@[protected, instance]
def pi.preconnected_space {ι : Type u_1} {π : ι Type u_2} [Π (i : ι), topological_space (π i)] [ (i : ι), preconnected_space (π i)] :
preconnected_space (Π (i : ι), π i)
@[protected, instance]
def pi.connected_space {ι : Type u_1} {π : ι Type u_2} [Π (i : ι), topological_space (π i)] [ (i : ι), connected_space (π i)] :
connected_space (Π (i : ι), π i)
@[protected, instance]
@[protected, instance]
theorem nonempty_inter {α : Type u} {s t : set α} :
theorem is_clopen_iff {α : Type u} {s : set α} :
s =
theorem is_clopen.eq_univ {α : Type u} {s : set α} (h' : is_clopen s) (h : s.nonempty) :
theorem frontier_eq_empty_iff {α : Type u} {s : set α} :
s =
theorem nonempty_frontier_iff {α : Type u} {s : set α} :
theorem subtype.preconnected_space {α : Type u} {s : set α} (h : is_preconnected s) :
theorem subtype.connected_space {α : Type u} {s : set α} (h : is_connected s) :
theorem is_preconnected_iff_preconnected_space {α : Type u} {s : set α} :
theorem is_connected_iff_connected_space {α : Type u} {s : set α} :
theorem is_preconnected_iff_subset_of_disjoint {α : Type u} {s : set α} :
(u v : set α), 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.

theorem is_connected_iff_sUnion_disjoint_open {α : Type u} {s : set α} :
(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.

theorem is_preconnected.subset_clopen {α : Type u} {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.

theorem disjoint_or_subset_of_clopen {α : Type u} {s t : set α} (hs : is_preconnected s) (ht : is_clopen t) :
t s t

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

theorem is_preconnected_iff_subset_of_disjoint_closed {α : Type u} {s : set α} :
(u v : set α), 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.

theorem is_preconnected_iff_subset_of_fully_disjoint_closed {α : Type u} {s : set α} (hs : is_closed s) :
(u v : set α), s u v 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 is_clopen.connected_component_subset {α : Type u} {s : set α} {x : α} (hs : is_clopen s) (hx : x s) :
theorem connected_component_subset_Inter_clopen {α : Type u} {x : α} :
(Z : {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.bUnion_connected_component_eq {α : Type u} {Z : set α} (h : is_clopen Z) :
( (x : α) (H : x Z), = Z

A clopen set is the union of its connected components.

theorem preimage_connected_component_connected {α : Type u} {β : Type v} {f : α β} (connected_fibers : (t : β), is_connected (f ⁻¹' {t})) (hcl : (T : set β), 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.

theorem quotient_map.preimage_connected_component {α : Type u} {β : Type v} {f : α β} (hf : quotient_map f) (h_fibers : (y : β), is_connected (f ⁻¹' {y})) (a : α) :
theorem quotient_map.image_connected_component {α : Type u} {β : Type v} {f : α β} (hf : quotient_map f) (h_fibers : (y : β), is_connected (f ⁻¹' {y})) (a : α) :
@[class]
structure locally_connected_space (α : Type u_3)  :
Prop

A topological space is locally connected if each neighborhood filter admits a basis of connected open sets. Note that it is equivalent to each point having a basis of connected (non necessarily open) sets but in a non-trivial way, so we choose this definition and prove the equivalence later in `locally_connected_space_iff_connected_basis`.

Instances of this typeclass
theorem locally_connected_space_iff_open_connected_basis {α : Type u}  :
(x : α), (nhds x).has_basis (λ (s : set α), x s id
theorem locally_connected_space_iff_open_connected_subsets {α : Type u}  :
(x : α) (U : set α), U nhds x ( (V : set α) (H : V U), x V
@[protected, instance]

A space with discrete topology is a locally connected space.

theorem connected_component_in_mem_nhds {α : Type u} {F : set α} {x : α} (h : F nhds x) :
theorem is_open.connected_component_in {α : Type u} {F : set α} {x : α} (hF : is_open F) :
theorem is_open_connected_component {α : Type u} {x : α} :
theorem is_clopen_connected_component {α : Type u} {x : α} :
theorem locally_connected_space_iff_connected_subsets {α : Type u}  :
(x : α) (U : set α), U nhds x ( (V : set α) (H : V nhds x), V U)
theorem locally_connected_space_iff_connected_basis {α : Type u}  :
(x : α), (nhds x).has_basis (λ (s : set α), s nhds x id
theorem locally_connected_space_of_connected_bases {α : Type u} {ι : Type u_1} (b : α ι set α) (p : α ι Prop) (hbasis : (x : α), (nhds x).has_basis (p x) (b x)) (hconnected : (x : α) (i : ι), p x i is_preconnected (b x i)) :
def is_totally_disconnected {α : Type u} (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
theorem is_totally_disconnected_singleton {α : Type u} {x : α} :
@[class]
structure totally_disconnected_space (α : Type u)  :
Prop
• is_totally_disconnected_univ :

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

Instances of this typeclass
theorem is_preconnected.subsingleton {α : Type u} {s : set α} (h : is_preconnected s) :
@[protected, instance]
def pi.totally_disconnected_space {α : Type u_1} {β : α Type u_2} [t₂ : Π (a : α), topological_space (β a)] [ (a : α), ] :
@[protected, instance]
def prod.totally_disconnected_space {α : Type u} {β : Type v}  :
@[protected, instance]
def sum.totally_disconnected_space {α : Type u} {β : Type v}  :
@[protected, instance]
def sigma.totally_disconnected_space {ι : Type u_1} {π : ι Type u_2} [Π (i : ι), topological_space (π i)] [ (i : ι), ] :
theorem is_totally_disconnected_of_clopen_set {X : Type u_1} (hX : {x y : X}, x y ( (U : set X) (h_clopen : , x U y U)) :

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 connected_component_eq_singleton {α : Type u} (x : α) :
= {x}
@[simp]
theorem continuous.image_connected_component_eq_singleton {α : Type u} {β : Type u_1} {f : α β} (h : continuous f) (a : α) :
= {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} {s : set α} {f : α β} (hf : s) (hf' : function.injective f) (h : is_totally_disconnected (f '' s)) :
theorem embedding.is_totally_disconnected {α : Type u} {β : Type v} {f : α β} (hf : embedding f) {s : set α} (h : is_totally_disconnected (f '' s)) :
@[protected, instance]
def subtype.totally_disconnected_space {α : Type u_1} {p : α Prop}  :
def is_totally_separated {α : Type u} (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
theorem is_totally_separated_empty {α : Type u}  :
theorem is_totally_separated_singleton {α : Type u} {x : α} :

Alias of `is_totally_disconnected_of_is_totally_separated`.

@[class]
structure totally_separated_space (α : Type u)  :
Prop
• is_totally_separated_univ :

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

Instances of this typeclass
@[protected, instance]
@[protected, instance]
theorem exists_clopen_of_totally_separated {α : Type u_1} {x y : α} (hxy : x y) :
(U : set α) (hU : , x U y U
def connected_component_setoid (α : Type u_1)  :

The setoid of connected components of a topological space

Equations
def connected_components (α : Type u)  :

The quotient of a space by its connected components

Equations
Instances for `connected_components`
@[protected, instance]
Equations
@[simp]
theorem connected_components.coe_eq_coe {α : Type u} {x y : α} :
theorem connected_components.coe_ne_coe {α : Type u} {x y : α} :
theorem connected_components.coe_eq_coe' {α : Type u} {x y : α} :
@[protected, instance]
Equations
@[protected, instance]
Equations
@[continuity]
@[simp]
theorem connected_components.range_coe {α : Type u}  :
theorem continuous.image_eq_of_connected_component_eq {α : Type u} {β : Type v} {f : α β} (h : continuous f) (a b : α) (hab : = ) :
f a = f b
def continuous.connected_components_lift {α : Type u} {β : Type v} {f : α β} (h : continuous f) :

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

Equations
@[continuity]
theorem continuous.connected_components_lift_continuous {α : Type u} {β : Type v} {f : α β} (h : continuous f) :
@[simp]
theorem continuous.connected_components_lift_apply_coe {α : Type u} {β : Type v} {f : α β} (h : continuous f) (x : α) :
= f x
@[simp]
theorem continuous.connected_components_lift_comp_coe {α : Type u} {β : Type v} {f : α β} (h : continuous f) :
theorem connected_components_lift_unique' {α : Type u} {β : Sort u_1} {g₁ g₂ : β} (hg : g₁ coe = g₂ coe) :
g₁ = g₂
theorem continuous.connected_components_lift_unique {α : Type u} {β : Type v} {f : α β} (h : continuous f) (g : β) (hg : g coe = f) :
theorem connected_components_preimage_singleton {α : Type u} {x : α} :

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} (U : set α) :
coe ⁻¹' (coe '' U) = (x : α) (H : x U),

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.

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

Functoriality of `connected_components`

Equations
theorem continuous.connected_components_map_continuous {α : Type u} {β : Type u_1} {f : α β} (h : continuous f) :
theorem is_preconnected.constant {α : Type u} {Y : Type u_1} {s : set α} (hs : is_preconnected s) {f : α Y} (hf : 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 is_preconnected_of_forall_constant {α : Type u} {s : set α} (hs : (f : α bool), (x : α), x s (y : α), y s f x = f y) :

If every map to `bool` (a discrete two-element space), that is continuous on a set `s`, is constant on s, then s is preconnected

theorem preconnected_space.constant {α : Type u} {Y : Type u_1} (hp : preconnected_space α) {f : α Y} (hf : continuous f) {x y : α} :
f x = f y

A `preconnected_space` version of `is_preconnected.constant`

theorem preconnected_space_of_forall_constant {α : Type u} (hs : (f : α bool), (x y : α), f x = f y) :

A `preconnected_space` version of `is_preconnected_of_forall_constant`

theorem is_preconnected.constant_of_maps_to {α : Type u} {β : Type v} {S : set α} (hS : is_preconnected S) {T : set β} {f : α β} (hc : S) (hTm : S T) {x y : α} (hx : x S) (hy : y S) :
f x = f y

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