mathlib documentation

topology.subset_properties

Properties of subsets of topological spaces

In this file we define various properties of subsets of a topological space, and some classes on topological spaces.

Main definitions

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

is_compact: each open cover has a finite subcover. This is defined in mathlib using filters. The main property of a compact set is is_compact.elim_finite_subcover.
is_clopen: a set that is both open and closed.
is_irreducible: a nonempty set that has contains no non-trivial pair of disjoint opens. See also the section below in the module doc.
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 (except for is_clopen), we also have a class stating that the whole space satisfies that property: compact_space, irreducible_space, connected_space, totally_disconnected_space, totally_separated_space.

Furthermore, we have two more classes:

locally_compact_space: for every point x, every open neighborhood of x contains a compact neighborhood of x. The definition is formulated in terms of the neighborhood filter.
sigma_compact_space: a space that is the union of a countably many compact subspaces.

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.

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

is_compact s = ∀ ⦃f : filter α⦄ [_inst_2 : f.ne_bot], f ≤ 𝓟 s → (∃ (a : α) (H : a ∈ s), cluster_pt a f)

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) :

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

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)) :

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.

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 set s has a neighborhood t within s such that p t, then p s holds.

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.

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.

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.

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

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

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

theorem compact_iff_ultrafilter_le_nhds {α : Type u} [topological_space α] {s : set α} :

is_compact s ↔ ∀ (f : ultrafilter α), ↑f ≤ 𝓟 s → (∃ (a : α) (H : a ∈ s), ↑f ≤ 𝓝 a)

theorem is_compact.ultrafilter_le_nhds {α : Type u} [topological_space α] {s : set α} :

is_compact s → ∀ (f : ultrafilter α), ↑f ≤ 𝓟 s → (∃ (a : α) (H : a ∈ s), ↑f ≤ 𝓝 a)

Alias of compact_iff_ultrafilter_le_nhds.

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.

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.

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.

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.

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.

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.

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) = ∅)) :

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.

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)) :

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

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.

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.

@[simp]

theorem compact_empty {α : Type u} [topological_space α] :

@[simp]

theorem compact_singleton {α : Type u} [topological_space α] {a : α} :

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)

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

is_compact (⋃ (i : β), f i)

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

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

is_compact (s ∪ t)

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

is_compact (insert a s)

def filter.cocompact (α : Type u_1) [topological_space α] :

filter.cocompact is the filter generated by complements to compact sets.

Equations

filter.cocompact α = ⨅ (s : set α) (hs : is_compact s), 𝓟 sᶜ

theorem filter.has_basis_cocompact {α : Type u} [topological_space α] :

(filter.cocompact α).has_basis is_compact compl

theorem filter.mem_cocompact {α : Type u} [topological_space α] {s : set α} :

s ∈ filter.cocompact α ↔ ∃ (t : set α), is_compact t ∧ tᶜ ⊆ s

theorem filter.mem_cocompact' {α : Type u} [topological_space α] {s : set α} :

s ∈ filter.cocompact α ↔ ∃ (t : set α), is_compact t ∧ sᶜ ⊆ t

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

sᶜ ∈ filter.cocompact α

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

nhds_contain_boxes s t = ∀ (n : set (α × β)), is_open n → s.prod t ⊆ n → (∃ (u : set α) (v : set β), is_open u ∧ is_open v ∧ s ⊆ u ∧ t ⊆ v ∧ u.prod v ⊆ n)

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

nhds_contain_boxes s t → nhds_contain_boxes t s

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

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

nhds_contain_boxes {x} {y}

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

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

If s and t are compact sets and n is an open neighborhood of s × t, then there exist open neighborhoods u ⊇ s and v ⊇ t such that u × v ⊆ n.

@[class]

structure compact_space (α : Type u_1) [topological_space α] :

Prop

compact_univ : is_compact set.univ

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

theorem compact_univ {α : Type u} [topological_space α] [h : compact_space α] :

is_compact set.univ

theorem cluster_point_of_compact {α : Type u} [topological_space α] [compact_space α] (f : filter α) [f.ne_bot] :

∃ (x : α), cluster_pt x f

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 α

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

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)

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)

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

is_compact (set.range f)

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

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)

theorem compact_iff_compact_in_subtype {α : Type u} [topological_space α] {p : α → Prop} {s : set {a // p a}} :

is_compact s ↔ is_compact (coe '' s)

theorem compact_iff_compact_univ {α : Type u} [topological_space α] {s : set α} :

is_compact s ↔ is_compact set.univ

theorem compact_iff_compact_space {α : Type u} [topological_space α] {s : set α} :

is_compact s ↔ compact_space ↥s

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)

@[instance]

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

compact_space α

Finite topological spaces are compact.

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

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

theorem compact_pi_infinite {ι : Type u_1} {π : ι → Type u_2} [Π (i : ι), topological_space («π» i)] {s : Π (i : ι), set («π» i)} :

(∀ (i : ι), is_compact (s i)) → is_compact {x : Π (i : ι), «π» i | ∀ (i : ι), x i ∈ s i}

Tychonoff's theorem

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.

@[instance]

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

compact_space (Π (i : ι), «π» i)

@[instance]

def quot.compact_space {α : Type u} [topological_space α] {r : α → α → Prop} [compact_space α] :

compact_space (quot r)

@[instance]

def quotient.compact_space {α : Type u} [topological_space α] {s : setoid α} [compact_space α] :

compact_space (quotient s)

@[class]

structure locally_compact_space (α : Type u_1) [topological_space α] :

Prop

local_compact_nhds : ∀ (x : α) (n : set α), n ∈ 𝓝 x → (∃ (s : set α) (H : s ∈ 𝓝 x), s ⊆ n ∧ is_compact s)

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

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.

theorem ultrafilter.le_nhds_Lim {α : Type u} [topological_space α] [compact_space α] (F : ultrafilter α) :

↑F ≤ 𝓝 (Lim ↑F)

@[class]

structure sigma_compact_space (α : Type u_1) [topological_space α] :

Prop

exists_compact_covering : ∃ (K : ℕ → set α), (∀ (n : ℕ), is_compact (K n)) ∧ (⋃ (n : ℕ), K n) = set.univ

A σ-compact space is a space that is the union of a countable collection of compact subspaces. Note that a locally compact separable T₂ space need not be σ-compact. The sequence can be extracted using topological_space.compact_covering.

Instances

separable_locally_compact_group.sigma_compact_space

def compact_covering (α : Type u) [topological_space α] [sigma_compact_space α] :

ℕ → set α

An arbitrary compact covering of a σ-compact space.

Equations

compact_covering α = classical.some sigma_compact_space.exists_compact_covering

theorem is_compact_compact_covering (α : Type u) [topological_space α] [sigma_compact_space α] (n : ℕ) :

is_compact (compact_covering α n)

theorem Union_compact_covering (α : Type u) [topological_space α] [sigma_compact_space α] :

(⋃ (n : ℕ), compact_covering α n) = set.univ

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

Prop

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

Equations

is_clopen s = (is_open s ∧ is_closed s)

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

is_clopen (s ∪ t)

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

is_clopen (s ∩ t)

@[simp]

theorem is_clopen_empty {α : Type u} [topological_space α] :

@[simp]

theorem is_clopen_univ {α : Type u} [topological_space α] :

is_clopen set.univ

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

@[simp]

theorem is_clopen_compl_iff {α : Type u} [topological_space α] {s : set α} :

is_clopen sᶜ ↔ is_clopen s

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

is_clopen (s \ t)

theorem is_clopen_Inter {α : Type u} [topological_space α] {β : Type u_1} [fintype β] {s : β → set α} (h : ∀ (i : β), is_clopen (s i)) :

is_clopen (⋂ (i : β), s i)

theorem is_clopen_bInter {α : Type u} [topological_space α] {β : Type u_1} {s : finset β} {f : β → set α} (h : ∀ (i : β), i ∈ s → is_clopen (f i)) :

is_clopen (⋂ (i : β) (H : i ∈ s), f i)

theorem continuous_on.preimage_clopen_of_clopen {α : Type u} [topological_space α] {β : Type u_1} [topological_space β] {f : α → β} {s : set α} {t : set β} (hf : continuous_on f s) (hs : is_clopen s) (ht : is_clopen t) :

is_clopen (s ∩ f ⁻¹' t)

theorem is_clopen_inter_of_disjoint_cover_clopen {α : Type u} [topological_space α] {Z a b : set α} (h : is_clopen Z) (cover : Z ⊆ a ∪ b) (ha : is_open a) (hb : is_open b) (hab : a ∩ b = ∅) :

is_clopen (Z ∩ a)

The intersection of a disjoint covering by two open sets of a clopen set will be clopen.

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

is_preirreducible s = ∀ (u v : set α), is_open u → is_open v → (s ∩ u).nonempty → (s ∩ v).nonempty → (s ∩ (u ∩ v)).nonempty

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

is_irreducible s = (s.nonempty ∧ is_preirreducible s)

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

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

is_preirreducible s

theorem is_preirreducible_empty {α : Type u} [topological_space α] :

is_preirreducible ∅

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

is_irreducible {x}

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

is_preirreducible (closure s)

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

is_irreducible (closure s)

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

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

set α

A maximal irreducible set that contains a given point.

Equations

irreducible_component x = classical.some _

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

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

x ∈ irreducible_component x

theorem is_irreducible_irreducible_component {α : Type u} [topological_space α] {x : α} :

is_irreducible (irreducible_component x)

theorem eq_irreducible_component {α : Type u} [topological_space α] {x : α} {s : set α} :

is_preirreducible s → irreducible_component x ⊆ s → s = irreducible_component x

theorem is_closed_irreducible_component {α : Type u} [topological_space α] {x : α} :

is_closed (irreducible_component x)

@[class]

structure preirreducible_space (α : Type u) [topological_space α] :

Prop

is_preirreducible_univ : is_preirreducible set.univ

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

Instances

irreducible_space.to_preirreducible_space

@[class]

structure irreducible_space (α : Type u) [topological_space α] :

Prop

to_preirreducible_space : preirreducible_space α
to_nonempty : nonempty α

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

theorem nonempty_preirreducible_inter {α : Type u} [topological_space α] [preirreducible_space α] {s t : set α} :

is_open s → is_open t → s.nonempty → t.nonempty → (s ∩ t).nonempty

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)

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)

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

preirreducible_space ↥s

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

irreducible_space ↥s

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

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.

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.

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

Prop

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

Equations

is_preconnected s = ∀ (u v : set α), is_open u → is_open v → s ⊆ u ∪ v → (s ∩ u).nonempty → (s ∩ v).nonempty → (s ∩ (u ∩ v)).nonempty

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

is_connected s = (s.nonempty ∧ is_preconnected s)

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) :

is_preconnected s

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

is_preconnected s

theorem is_irreducible.is_connected {α : Type u} [topological_space α] {s : set α} (H : is_irreducible s) :

theorem is_preconnected_empty {α : Type u} [topological_space α] :

is_preconnected ∅

theorem is_connected_singleton {α : Type u} [topological_space α] {x : α} :

is_connected {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)) :

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.

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.

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.

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)

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)

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

is_preconnected (closure s)

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

is_connected (closure 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) :

is_preconnected (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) :

is_connected (f '' s)

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

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

connected_component x = ⋃₀{s : set α | is_preconnected s ∧ x ∈ s}

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

set α

The connected component of a point inside a set.

Equations

connected_component_in F x = coe '' connected_component x

theorem mem_connected_component {α : Type u} [topological_space α] {x : α} :

x ∈ connected_component x

theorem is_connected_connected_component {α : Type u} [topological_space α] {x : α} :

is_connected (connected_component x)

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

s ⊆ connected_component x

theorem is_closed_connected_component {α : Type u} [topological_space α] {x : α} :

is_closed (connected_component x)

theorem irreducible_component_subset_connected_component {α : Type u} [topological_space α] {x : α} :

irreducible_component x ⊆ connected_component x

@[class]

structure preconnected_space (α : Type u) [topological_space α] :

Prop

is_preconnected_univ : is_preconnected set.univ

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

Instances

@[class]

structure connected_space (α : Type u) [topological_space α] :

Prop

to_preconnected_space : preconnected_space α
to_nonempty : nonempty α

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) :

is_connected (set.range f)

theorem connected_space_iff_connected_component {α : Type u} [topological_space α] :

connected_space α ↔ ∃ (x : α), connected_component x = set.univ

@[instance]

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

preconnected_space α

@[instance]

def irreducible_space.connected_space (α : Type u) [topological_space α] [irreducible_space α] :

connected_space α

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

theorem is_clopen_iff {α : Type u} [topological_space α] [preconnected_space α] {s : set α} :

is_clopen s ↔ s = ∅ ∨ s = set.univ

theorem eq_univ_of_nonempty_clopen {α : Type u} [topological_space α] [preconnected_space α] {s : set α} (h : s.nonempty) (h' : is_clopen s) :

theorem subtype.preconnected_space {α : Type u} [topological_space α] {s : set α} (h : is_preconnected s) :

preconnected_space ↥s

theorem subtype.connected_space {α : Type u} [topological_space α] {s : set α} (h : is_connected s) :

connected_space ↥s

theorem is_preconnected_iff_preconnected_space {α : Type u} [topological_space α] {s : set α} :

is_preconnected s ↔ preconnected_space ↥s

theorem is_connected_iff_connected_space {α : Type u} [topological_space α] {s : set α} :

is_connected s ↔ connected_space ↥s

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.

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.

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

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.

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.

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

is_totally_disconnected s = ∀ (t : set α), t ⊆ s → is_preconnected t → subsingleton ↥t

theorem is_totally_disconnected_empty {α : Type u} [topological_space α] :

is_totally_disconnected ∅

theorem is_totally_disconnected_singleton {α : Type u} [topological_space α] {x : α} :

is_totally_disconnected {x}

@[class]

structure totally_disconnected_space (α : Type u) [topological_space α] :

Prop

is_totally_disconnected_univ : is_totally_disconnected set.univ

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

Instances

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

@[instance]

def subtype.totally_disconnected_space {α : Type u_1} {p : α → Prop} [topological_space α] [totally_disconnected_space α] :

totally_disconnected_space (subtype p)

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

is_totally_separated s = ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x ≠ y → (∃ (u v : set α), is_open u ∧ is_open v ∧ x ∈ u ∧ y ∈ v ∧ s ⊆ u ∪ v ∧ u ∩ v = ∅)

theorem is_totally_separated_empty {α : Type u} [topological_space α] :

is_totally_separated ∅

theorem is_totally_separated_singleton {α : Type u} [topological_space α] {x : α} :

is_totally_separated {x}

theorem is_totally_disconnected_of_is_totally_separated {α : Type u} [topological_space α] {s : set α} (H : is_totally_separated s) :

is_totally_disconnected s

@[class]

structure totally_separated_space (α : Type u) [topological_space α] :

Prop

is_totally_separated_univ : is_totally_separated set.univ

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

Instances

totally_separated_space.of_discrete

@[instance]

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

totally_disconnected_space α

@[instance]

def totally_separated_space.of_discrete (α : Type u_1) [topological_space α] [discrete_topology α] :

totally_separated_space α