mathlib documentation

topology.subset_properties

Properties of subsets of topological spaces

Main definitions

compact, is_clopen, is_irreducible, is_connected, is_totally_disconnected, is_totally_separated

TODO: write better docs

On the definition of irreducible and connected sets/spaces

In informal mathematics, irreducible and connected spaces are assumed to be nonempty. We formalise the predicate without that assumption as is_preirreducible and is_preconnected respectively. In other words, the only difference is whether the empty space counts as irreducible and/or 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_compact {α : Type u} [topological_space α] (s : set α) :
Prop

A set s is compact if for every filter f that contains s, every set of f also meets every neighborhood of some a ∈ s.

Equations
source
theorem is_compact.compl_mem_sets {α : Type u} [topological_space α] {s : set α} (hs : is_compact s) {f : filter α} (hf : ∀ (a : α), a ∈ s → sᶜ ∈ 𝓝 a ⊓ f) :
sᶜ ∈ f

The complement to a compact set belongs to a filter f if it belongs to each filter 𝓝 a ⊓ f, a ∈ s.

source
theorem is_compact.compl_mem_sets_of_nhds_within {α : Type u} [topological_space α] {s : set α} (hs : is_compact s) {f : filter α} (hf : ∀ (a : α), a ∈ s → (∃ (t : set α) (H : t ∈ 𝓝[s] a), tᶜ ∈ f)) :
sᶜ ∈ f

The complement to a compact set belongs to a filter f if each a ∈ s has a neighborhood t within s such that tᶜ belongs to f.

source
theorem is_compact.induction_on {α : Type u} [topological_space α] {s : set α} (hs : is_compact s) {p : set α → Prop} (he : p ∅) (hmono : ∀ ⦃s t : set α⦄, s ⊆ t → p t → p s) (hunion : ∀ ⦃s t : set α⦄, p s → p t → p (s ∪ t)) (hnhds : ∀ (x : α), x ∈ s → (∃ (t : set α) (H : t ∈ 𝓝[s] x), p t)) :
p s

If p : set α → Prop is stable under restriction and union, and each point x of a compact sets has a neighborhoodtwithinssuch thatp t, thenp s` holds.

source
theorem is_compact.inter_right {α : Type u} [topological_space α] {s t : set α} (hs : is_compact s) (ht : is_closed t) :
is_compact (s ∩ t)

The intersection of a compact set and a closed set is a compact set.

source
theorem is_compact.inter_left {α : Type u} [topological_space α] {s t : set α} (ht : is_compact t) (hs : is_closed s) :
is_compact (s ∩ t)

The intersection of a closed set and a compact set is a compact set.

source
theorem compact_diff {α : Type u} [topological_space α] {s t : set α} (hs : is_compact s) (ht : is_open t) :
is_compact (s \ t)

The set difference of a compact set and an open set is a compact set.

source
theorem compact_of_is_closed_subset {α : Type u} [topological_space α] {s t : set α} (hs : is_compact s) (ht : is_closed t) (h : t ⊆ s) :
is_compact t

A closed subset of a compact set is a compact set.

source
theorem is_compact.adherence_nhdset {α : Type u} [topological_space α] {s t : set α} {f : filter α} (hs : is_compact s) (hf₂ : f ≤ 𝓟 s) (ht₁ : is_open t) (ht₂ : ∀ (a : α), a ∈ s → cluster_pt a f → a ∈ t) :
t ∈ f

source
theorem compact_iff_ultrafilter_le_nhds {α : Type u} [topological_space α] {s : set α} :
is_compact s ↔ ∀ (f : filter α), f.is_ultrafilter → f ≤ 𝓟 s → (∃ (a : α) (H : a ∈ s), f ≤ 𝓝 a)

source
theorem is_compact.elim_finite_subcover {α : Type u} [topological_space α] {s : set α} {ι : Type v} (hs : is_compact s) (U : ι → set α) (hUo : ∀ (i : ι), is_open (U i)) (hsU : s ⊆ ⋃ (i : ι), U i) :
∃ (t : finset ι), s ⊆ ⋃ (i : ι) (H : i ∈ t), U i

For every open cover of a compact set, there exists a finite subcover.

source
theorem is_compact.elim_finite_subfamily_closed {α : Type u} [topological_space α] {s : set α} {ι : Type v} (hs : is_compact s) (Z : ι → set α) (hZc : ∀ (i : ι), is_closed (Z i)) (hsZ : (s ∩ ⋂ (i : ι), Z i) = ∅) :
∃ (t : finset ι), (s ∩ ⋂ (i : ι) (H : i ∈ t), Z i) = ∅

For every family of closed sets whose intersection avoids a compact set, there exists a finite subfamily whose intersection avoids this compact set.

source
theorem is_compact.inter_Inter_nonempty {α : Type u} [topological_space α] {s : set α} {ι : Type v} (hs : is_compact s) (Z : ι → set α) (hZc : ∀ (i : ι), is_closed (Z i)) (hsZ : ∀ (t : finset ι), (s ∩ ⋂ (i : ι) (H : i ∈ t), Z i).nonempty) :
(s ∩ ⋂ (i : ι), Z i).nonempty

To show that a compact set intersects the intersection of a family of closed sets, it is sufficient to show that it intersects every finite subfamily.

source
theorem is_compact.nonempty_Inter_of_directed_nonempty_compact_closed {α : Type u} [topological_space α] {ι : Type v} [hι : nonempty ι] (Z : ι → set α) (hZd : directed superset Z) (hZn : ∀ (i : ι), (Z i).nonempty) (hZc : ∀ (i : ι), is_compact (Z i)) (hZcl : ∀ (i : ι), is_closed (Z i)) :
(⋂ (i : ι), Z i).nonempty

Cantor's intersection theorem: the intersection of a directed family of nonempty compact closed sets is nonempty.

source
theorem is_compact.nonempty_Inter_of_sequence_nonempty_compact_closed {α : Type u} [topological_space α] (Z : ℕ → set α) (hZd : ∀ (i : ℕ), Z (i + 1) ⊆ Z i) (hZn : ∀ (i : ℕ), (Z i).nonempty) (hZ0 : is_compact (Z 0)) (hZcl : ∀ (i : ℕ), is_closed (Z i)) :
(⋂ (i : ℕ), Z i).nonempty

Cantor's intersection theorem for sequences indexed by ℕ: the intersection of a decreasing sequence of nonempty compact closed sets is nonempty.

source
theorem is_compact.elim_finite_subcover_image {α : Type u} {β : Type v} [topological_space α] {s : set α} {b : set β} {c : β → set α} (hs : is_compact s) (hc₁ : ∀ (i : β), i ∈ b → is_open (c i)) (hc₂ : s ⊆ ⋃ (i : β) (H : i ∈ b), c i) :
∃ (b' : set β) (H : b' ⊆ b), b'.finite ∧ s ⊆ ⋃ (i : β) (H : i ∈ b'), c i

For every open cover of a compact set, there exists a finite subcover.

source
theorem compact_of_finite_subfamily_closed {α : Type u} [topological_space α] {s : set α} (h : ∀ {ι : Type u} (Z : ι → set α), (∀ (i : ι), is_closed (Z i)) → (s ∩ ⋂ (i : ι), Z i) = ∅ → (∃ (t : finset ι), (s ∩ ⋂ (i : ι) (H : i ∈ t), Z i) = ∅)) :
is_compact s

A set s is compact if for every family of closed sets whose intersection avoids s, there exists a finite subfamily whose intersection avoids s.

source
theorem compact_of_finite_subcover {α : Type u} [topological_space α] {s : set α} (h : ∀ {ι : Type u} (U : ι → set α), (∀ (i : ι), is_open (U i)) → (s ⊆ ⋃ (i : ι), U i) → (∃ (t : finset ι), s ⊆ ⋃ (i : ι) (H : i ∈ t), U i)) :
is_compact s

A set s is compact if for every open cover of s, there exists a finite subcover.

source
theorem compact_iff_finite_subcover {α : Type u} [topological_space α] {s : set α} :
is_compact s ↔ ∀ {ι : Type u} (U : ι → set α), (∀ (i : ι), is_open (U i)) → (s ⊆ ⋃ (i : ι), U i) → (∃ (t : finset ι), s ⊆ ⋃ (i : ι) (H : i ∈ t), U i)

A set s is compact if and only if for every open cover of s, there exists a finite subcover.

source
theorem compact_iff_finite_subfamily_closed {α : Type u} [topological_space α] {s : set α} :
is_compact s ↔ ∀ {ι : Type u} (Z : ι → set α), (∀ (i : ι), is_closed (Z i)) → (s ∩ ⋂ (i : ι), Z i) = ∅ → (∃ (t : finset ι), (s ∩ ⋂ (i : ι) (H : i ∈ t), Z i) = ∅)

A set s is compact if and only if for every family of closed sets whose intersection avoids s, there exists a finite subfamily whose intersection avoids s.

source
@[simp]
theorem compact_empty {α : Type u} [topological_space α] :
is_compact ∅

source
@[simp]
theorem compact_singleton {α : Type u} [topological_space α] {a : α} :
is_compact {a}

source
theorem set.finite.compact_bUnion {α : Type u} {β : Type v} [topological_space α] {s : set β} {f : β → set α} (hs : s.finite) (hf : ∀ (i : β), i ∈ s → is_compact (f i)) :
is_compact (⋃ (i : β) (H : i ∈ s), f i)

source
theorem compact_Union {α : Type u} {β : Type v} [topological_space α] {f : β → set α} [fintype β] (h : ∀ (i : β), is_compact (f i)) :
is_compact (⋃ (i : β), f i)

source
theorem set.finite.is_compact {α : Type u} [topological_space α] {s : set α} (hs : s.finite) :
is_compact s

source
theorem is_compact.union {α : Type u} [topological_space α] {s t : set α} (hs : is_compact s) (ht : is_compact t) :
is_compact (s ∪ t)

source
def nhds_contain_boxes {α : Type u} {β : Type v} [topological_space α] [topological_space β] (s : set α) (t : set β) :
Prop

nhds_contain_boxes s t means that any open neighborhood of s × t in α × β includes a product of an open neighborhood of s by an open neighborhood of t.

Equations
source
theorem nhds_contain_boxes.symm {α : Type u} {β : Type v} [topological_space α] [topological_space β] {s : set α} {t : set β} (a : nhds_contain_boxes s t) :
nhds_contain_boxes t s

source
theorem nhds_contain_boxes.comm {α : Type u} {β : Type v} [topological_space α] [topological_space β] {s : set α} {t : set β} :
nhds_contain_boxes s t ↔ nhds_contain_boxes t s

source
theorem nhds_contain_boxes_of_singleton {α : Type u} {β : Type v} [topological_space α] [topological_space β] {x : α} {y : β} :
nhds_contain_boxes {x} {y}

source
theorem nhds_contain_boxes_of_compact {α : Type u} {β : Type v} [topological_space α] [topological_space β] {s : set α} (hs : is_compact s) (t : set β) (H : ∀ (x : α), x ∈ s → nhds_contain_boxes {x} t) :
nhds_contain_boxes s t

source
theorem generalized_tube_lemma {α : Type u} {β : Type v} [topological_space α] [topological_space β] {s : set α} (hs : is_compact s) {t : set β} (ht : is_compact t) {n : set (α × β)} (hn : is_open n) (hp : s.prod t ⊆ n) :
∃ (u : set α) (v : set β), is_open u ∧ is_open v ∧ s ⊆ u ∧ t ⊆ v ∧ u.prod v ⊆ n

source
@[class]
structure compact_space (α : Type u_1) [topological_space α] :
Prop

Type class for compact spaces. Separation is sometimes included in the definition, especially in the French literature, but we do not include it here.

Instances
source
theorem compact_univ {α : Type u} [topological_space α] [h : compact_space α] :
is_compact set.univ

source
theorem cluster_point_of_compact {α : Type u} [topological_space α] [compact_space α] (f : filter α) [f.ne_bot] :
∃ (x : α), cluster_pt x f

source
theorem compact_space_of_finite_subfamily_closed {α : Type u} [topological_space α] (h : ∀ {ι : Type u} (Z : ι → set α), (∀ (i : ι), is_closed (Z i)) → (⋂ (i : ι), Z i) = ∅ → (∃ (t : finset ι), (⋂ (i : ι) (H : i ∈ t), Z i) = ∅)) :
compact_space α

source
theorem is_closed.compact {α : Type u} [topological_space α] [compact_space α] {s : set α} (h : is_closed s) :
is_compact s

source
theorem is_compact.image_of_continuous_on {α : Type u} {β : Type v} [topological_space α] {s : set α} [topological_space β] {f : α → β} (hs : is_compact s) (hf : continuous_on f s) :
is_compact (f '' s)

source
theorem is_compact.image {α : Type u} {β : Type v} [topological_space α] {s : set α} [topological_space β] {f : α → β} (hs : is_compact s) (hf : continuous f) :
is_compact (f '' s)

source
theorem compact_range {α : Type u} {β : Type v} [topological_space α] [topological_space β] [compact_space α] {f : α → β} (hf : continuous f) :
is_compact (set.range f)

source
theorem is_closed_proj_of_compact {X : Type u_1} [topological_space X] [compact_space X] {Y : Type u_2} [topological_space Y] :
is_closed_map prod.snd

If X is is_compact then pr₂ : X × Y → Y is a closed map

source
theorem embedding.compact_iff_compact_image {α : Type u} {β : Type v} [topological_space α] {s : set α} [topological_space β] {f : α → β} (hf : embedding f) :
is_compact s ↔ is_compact (f '' s)

source
theorem compact_iff_compact_in_subtype {α : Type u} [topological_space α] {p : α → Prop} {s : set {a // p a}} :
is_compact s ↔ is_compact (coe '' s)

source
theorem compact_iff_compact_univ {α : Type u} [topological_space α] {s : set α} :
is_compact s ↔ is_compact set.univ

source
theorem compact_iff_compact_space {α : Type u} [topological_space α] {s : set α} :
is_compact s ↔ compact_space ↥s

source
theorem is_compact.prod {α : Type u} {β : Type v} [topological_space α] [topological_space β] {s : set α} {t : set β} (hs : is_compact s) (ht : is_compact t) :
is_compact (s.prod t)

source
@[instance]
def fintype.compact_space {α : Type u} [topological_space α] [fintype α] :
compact_space α

Finite topological spaces are compact.

source
@[instance]
def prod.compact_space {α : Type u} {β : Type v} [topological_space α] [topological_space β] [compact_space α] [compact_space β] :
compact_space (α × β)

The product of two compact spaces is compact.

source
@[instance]
def sum.compact_space {α : Type u} {β : Type v} [topological_space α] [topological_space β] [compact_space α] [compact_space β] :
compact_space (α ⊕ β)

The disjoint union of two compact spaces is compact.

source
theorem compact_pi_infinite {ι : Type u_1} {π : ι → Type u_2} [Π (i : ι), topological_space («π» i)] {s : Π (i : ι), set («π» i)} (a : ∀ (i : ι), is_compact (s i)) :
is_compact {x : Π (i : ι), «π» i | ∀ (i : ι), x i ∈ s i}

Tychonoff's theorem

source
theorem compact_univ_pi {ι : Type u_1} {π : ι → Type u_2} [Π (i : ι), topological_space («π» i)] {s : Π (i : ι), set («π» i)} (h : ∀ (i : ι), is_compact (s i)) :
is_compact (set.univ.pi s)

A version of Tychonoff's theorem that uses set.pi.

source
@[instance]
def pi.compact {ι : Type u_1} {π : ι → Type u_2} [Π (i : ι), topological_space («π» i)] [∀ (i : ι), compact_space («π» i)] :
compact_space (Π (i : ι), «π» i)

source
@[instance]
def quot.compact_space {α : Type u} [topological_space α] {r : α → α → Prop} [compact_space α] :
compact_space (quot r)

source
@[instance]
def quotient.compact_space {α : Type u} [topological_space α] {s : setoid α} [compact_space α] :
compact_space (quotient s)

source
@[class]
structure locally_compact_space (α : Type u_1) [topological_space α] :
Prop

There are various definitions of "locally compact space" in the literature, which agree for Hausdorff spaces but not in general. This one is the precise condition on X needed for the evaluation map C(X, Y) × X → Y to be continuous for all Y when C(X, Y) is given the compact-open topology.

Instances
source
theorem exists_compact_subset {α : Type u} [topological_space α] [locally_compact_space α] {x : α} {U : set α} (hU : is_open U) (hx : x ∈ U) :
∃ (K : set α), is_compact K ∧ x ∈ interior K ∧ K ⊆ U

A reformulation of the definition of locally compact space: In a locally compact space, every open set containing x has a compact subset containing x in its interior.

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

A set is clopen if it is both open and closed.

Equations
source
theorem is_clopen_union {α : Type u} [topological_space α] {s t : set α} (hs : is_clopen s) (ht : is_clopen t) :
is_clopen (s ∪ t)

source
theorem is_clopen_inter {α : Type u} [topological_space α] {s t : set α} (hs : is_clopen s) (ht : is_clopen t) :
is_clopen (s ∩ t)

source
@[simp]
theorem is_clopen_empty {α : Type u} [topological_space α] :
is_clopen ∅

source
@[simp]
theorem is_clopen_univ {α : Type u} [topological_space α] :
is_clopen set.univ

source
theorem is_clopen_compl {α : Type u} [topological_space α] {s : set α} (hs : is_clopen s) :
is_clopen sᶜ

source
@[simp]
theorem is_clopen_compl_iff {α : Type u} [topological_space α] {s : set α} :
is_clopen sᶜ ↔ is_clopen s

source
theorem is_clopen_diff {α : Type u} [topological_space α] {s t : set α} (hs : is_clopen s) (ht : is_clopen t) :
is_clopen (s \ t)

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

A preirreducible set s is one where there is no non-trivial pair of disjoint opens on s.

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

An irreducible set s is one that is nonempty and where there is no non-trivial pair of disjoint opens on s.

Equations
source
theorem is_irreducible.nonempty {α : Type u} [topological_space α] {s : set α} (h : is_irreducible s) :
s.nonempty

source
theorem is_irreducible.is_preirreducible {α : Type u} [topological_space α] {s : set α} (h : is_irreducible s) :
is_preirreducible s

source
theorem is_preirreducible_empty {α : Type u} [topological_space α] :
is_preirreducible ∅

source
theorem is_irreducible_singleton {α : Type u} [topological_space α] {x : α} :
is_irreducible {x}

source
theorem is_preirreducible.closure {α : Type u} [topological_space α] {s : set α} (H : is_preirreducible s) :
is_preirreducible (closure s)

source
theorem is_irreducible.closure {α : Type u} [topological_space α] {s : set α} (h : is_irreducible s) :
is_irreducible (closure s)

source
theorem exists_preirreducible {α : Type u} [topological_space α] (s : set α) (H : is_preirreducible s) :
∃ (t : set α), is_preirreducible t ∧ s ⊆ t ∧ ∀ (u : set α), is_preirreducible u → t ⊆ u → u = t

source
def irreducible_component {α : Type u} [topological_space α] (x : α) :
set α

A maximal irreducible set that contains a given point.

Equations
source
theorem irreducible_component_property {α : Type u} [topological_space α] (x : α) :
is_preirreducible (irreducible_component x) ∧ {x} ⊆ irreducible_component x ∧ ∀ (u : set α), is_preirreducible u → irreducible_component x ⊆ u → u = irreducible_component x

source
theorem mem_irreducible_component {α : Type u} [topological_space α] {x : α} :
x ∈ irreducible_component x

source
theorem is_irreducible_irreducible_component {α : Type u} [topological_space α] {x : α} :
is_irreducible (irreducible_component x)

source
theorem eq_irreducible_component {α : Type u} [topological_space α] {x : α} {s : set α} (a : is_preirreducible s) (a_1 : irreducible_component x ⊆ s) :
s = irreducible_component x

source
theorem is_closed_irreducible_component {α : Type u} [topological_space α] {x : α} :
is_closed (irreducible_component x)

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

A preirreducible space is one where there is no non-trivial pair of disjoint opens.

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

An irreducible space is one that is nonempty and where there is no non-trivial pair of disjoint opens.

source
theorem nonempty_preirreducible_inter {α : Type u} [topological_space α] [preirreducible_space α] {s t : set α} (a : is_open s) (a_1 : is_open t) (a_2 : s.nonempty) (a_3 : t.nonempty) :
(s ∩ t).nonempty

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

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

source
theorem subtype.preirreducible_space {α : Type u} [topological_space α] {s : set α} (h : is_preirreducible s) :
preirreducible_space ↥s

source
theorem subtype.irreducible_space {α : Type u} [topological_space α] {s : set α} (h : is_irreducible s) :
irreducible_space ↥s

source
theorem is_irreducible_iff_sInter {α : Type u} [topological_space α] {s : set α} :
is_irreducible s ↔ ∀ (U : finset (set α)), (∀ (u : set α), u ∈ U → is_open u) → (∀ (u : set α), u ∈ U → (s ∩ u).nonempty) → (s ∩ ⋂₀↑U).nonempty

A set s is irreducible if and only if for every finite collection of open sets all of whose members intersect s, s also intersects the intersection of the entire collection (i.e., there is an element of s contained in every member of the collection).

source
theorem is_preirreducible_iff_closed_union_closed {α : Type u} [topological_space α] {s : set α} :
is_preirreducible s ↔ ∀ (z₁ z₂ : set α), is_closed z₁ → is_closed z₂ → s ⊆ z₁ ∪ z₂ → s ⊆ z₁ ∨ s ⊆ z₂

A set is preirreducible if and only if for every cover by two closed sets, it is contained in one of the two covering sets.

source
theorem is_irreducible_iff_sUnion_closed {α : Type u} [topological_space α] {s : set α} :
is_irreducible s ↔ ∀ (Z : finset (set α)), (∀ (z : set α), z ∈ Z → is_closed z) → s ⊆ ⋃₀↑Z → (∃ (z : set α) (H : z ∈ Z), s ⊆ z)

A set is irreducible if and only if for every cover by a finite collection of closed sets, it is contained in one of the members of the collection.

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_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 y : α), x ∈ s → 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 α] (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_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.closure {α : Type u} [topological_space α] {s : set α} (H : is_preconnected s) :
is_preconnected (closure s)

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)

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
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_connected_connected_component {α : Type u} [topological_space α] {x : α} :
is_connected (connected_component x)

source
theorem subset_connected_component {α : Type u} [topological_space α] {x : α} {s : set α} (H1 : is_preconnected s) (H2 : x ∈ s) :
s ⊆ connected_component x

source
theorem is_closed_connected_component {α : Type u} [topological_space α] {x : α} :
is_closed (connected_component x)

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_range {α : Type u} {β : Type v} [topological_space α] [topological_space β] [connected_space α] {f : α → β} (h : continuous f) :
is_connected (set.range f)

source
theorem connected_space_iff_connected_component {α : Type u} [topological_space α] :
connected_space α ↔ ∃ (x : α), connected_component x = set.univ

source
@[instance]
def preirreducible_space.preconnected_space (α : Type u) [topological_space α] [preirreducible_space α] :
preconnected_space α

source
@[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 α} (a : is_open s) (a_1 : is_open t) (a_2 : s ∪ t = set.univ) (a_3 : s.nonempty) (a_4 : 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 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
def is_totally_disconnected {α : Type u} [topological_space α] (s : set α) :
Prop

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

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

source
@[instance]
def totally_separated_space.totally_disconnected_space (α : Type u) [topological_space α] [totally_separated_space α] :
totally_disconnected_space α