mathlib documentation

topology.​subset_properties

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.

def is_compact {α : Type u} [topological_space α] :
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
theorem is_compact.​compl_mem_sets {α : Type u} [topological_space α] {s : set α} (hs : is_compact s) {f : filter α} :
(∀ (a : α), a ss nhds 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.

theorem is_compact.​compl_mem_sets_of_nhds_within {α : Type u} [topological_space α] {s : set α} (hs : is_compact s) {f : filter α} :
(∀ (a : α), a s(∃ (t : set α) (H : t nhds_within a s), 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.

theorem is_compact.​induction_on {α : Type u} [topological_space α] {s : set α} (hs : is_compact s) {p : set α → Prop} :
p (∀ ⦃s t : set α⦄, s tp tp s)(∀ ⦃s t : set α⦄, p sp tp (s t))(∀ (x : α), x s(∃ (t : set α) (H : t nhds_within x s), 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.

theorem is_compact.​inter_right {α : Type u} [topological_space α] {s t : set α} :

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 α} :

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

theorem compact_diff {α : Type u} [topological_space α] {s t : set α} :
is_compact sis_open tis_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 α} :
is_compact sis_closed tt sis_compact t

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 α} :
is_compact sf filter.principal sis_open t(∀ (a : α), a scluster_pt a fa t)t f

theorem compact_iff_ultrafilter_le_nhds {α : Type u} [topological_space α] {s : set α} :
is_compact s ∀ (f : filter α), f.is_ultrafilterf filter.principal s(∃ (a : α) (H : a s), f nhds a)

theorem is_compact.​elim_finite_subcover {α : Type u} [topological_space α] {s : set α} {ι : Type v} (hs : is_compact s) (U : ι → set α) :
(∀ (i : ι), is_open (U i))(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 α) :
(∀ (i : ι), is_closed (Z i))(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 α) :
(∀ (i : ι), is_closed (Z i))(∀ (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 α) :
directed superset Z(∀ (i : ι), (Z i).nonempty)(∀ (i : ι), is_compact (Z i))(∀ (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 α) :
(∀ (i : ), Z (i + 1) Z i)(∀ (i : ), (Z i).nonempty)is_compact (Z 0)(∀ (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 α} :
is_compact s(∀ (i : β), i bis_open (c i))(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 α} :
(∀ {ι : 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.

theorem compact_of_finite_subcover {α : Type u} [topological_space α] {s : set α} :
(∀ {ι : 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.

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 α} :
s.finite(∀ (i : β), i sis_compact (f i))is_compact (⋃ (i : β) (H : i s), f i)

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

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

theorem is_compact.​union {α : Type u} [topological_space α] {s t : set α} :

def nhds_contain_boxes {α : Type u} {β : Type v} [topological_space α] [topological_space β] :
set α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
theorem nhds_contain_boxes.​symm {α : Type u} {β : Type v} [topological_space α] [topological_space β] {s : set α} {t : set β} :

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

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

theorem nhds_contain_boxes_of_compact {α : Type u} {β : Type v} [topological_space α] [topological_space β] {s : set α} (hs : is_compact s) (t : set β) :
(∀ (x : α), x snhds_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 × β)} :
is_open ns.prod t n(∃ (u : set α) (v : set β), is_open u is_open v s u t v u.prod v n)

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

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 α] :
(∀ {ι : 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 α} :

theorem is_compact.​image_of_continuous_on {α : Type u} {β : Type v} [topological_space α] {s : set α} [topological_space β] {f : α → β} :

theorem is_compact.​image {α : Type u} {β : Type v} [topological_space α] {s : set α} [topological_space β] {f : α → β} :

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

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 : α → β} :

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

theorem is_compact.​prod {α : Type u} {β : Type v} [topological_space α] [topological_space β] {s : set α} {t : set β} :

@[instance]

Finite topological spaces are compact.

Equations
@[instance]
def prod.​compact_space {α : Type u} {β : Type v} [topological_space α] [topological_space β] [compact_space α] [compact_space β] :

The product of two compact spaces is compact.

Equations
@[instance]
def sum.​compact_space {α : Type u} {β : Type v} [topological_space α] [topological_space β] [compact_space α] [compact_space β] :

The disjoint union of two compact spaces is compact.

Equations
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)} :
(∀ (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)

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

Equations
@[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
theorem exists_compact_subset {α : Type u} [topological_space α] [locally_compact_space α] {x : α} {U : set α} :
is_open Ux 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.

def is_clopen {α : Type u} [topological_space α] :
set α → Prop

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

Equations
theorem is_clopen_union {α : Type u} [topological_space α] {s t : set α} :
is_clopen sis_clopen tis_clopen (s t)

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

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

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

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

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

theorem is_clopen_diff {α : Type u} [topological_space α] {s t : set α} :
is_clopen sis_clopen tis_clopen (s \ t)

def is_preirreducible {α : Type u} [topological_space α] :
set α → Prop

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

Equations
def is_irreducible {α : Type u} [topological_space α] :
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
theorem is_irreducible.​nonempty {α : Type u} [topological_space α] {s : set α} :

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

theorem exists_preirreducible {α : Type u} [topological_space α] (s : set α) :
is_preirreducible s(∃ (t : set α), is_preirreducible t s t ∀ (u : set α), is_preirreducible ut uu = t)

def irreducible_component {α : Type u} [topological_space α] :
α → set α

A maximal irreducible set that contains a given point.

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

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

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

theorem nonempty_preirreducible_inter {α : Type u} [topological_space α] [preirreducible_space α] {s t : set α} :
is_open sis_open ts.nonemptyt.nonempty(s t).nonempty

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

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

theorem is_irreducible_iff_sInter {α : Type u} [topological_space α] {s : set α} :
is_irreducible s ∀ (U : finset (set α)), (∀ (u : set α), u Uis_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 Zis_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 α] :
set α → Prop

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

Equations
def is_connected {α : Type u} [topological_space α] :
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 α} :

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

theorem is_preconnected_of_forall {α : Type u} [topological_space α] {s : set α} (x : α) :
(∀ (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 α} :
(∀ (x y : α), x sy 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 α)) :
(∀ (s : set α), s cx s)(∀ (s : set α), s cis_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 α} :
x sx tis_preconnected sis_preconnected tis_preconnected (s t)

theorem is_connected.​union {α : Type u} [topological_space α] {s t : set α} :

theorem is_connected.​closure {α : Type u} [topological_space α] {s : set α} :

theorem is_preconnected.​image {α : Type u} {β : Type v} [topological_space α] [topological_space β] {s : set α} (H : is_preconnected s) (f : α → β) :

theorem is_connected.​image {α : Type u} {β : Type v} [topological_space α] [topological_space β] {s : set α} (H : is_connected s) (f : α → β) :

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 α] :
α → 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 α) :
F → set α

The connected component of a point inside a set.

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

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

@[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 : α → β} :

@[instance]

Equations
  • _ = _
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 α} :

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.

def is_totally_disconnected {α : Type u} [topological_space α] :
set α → Prop

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

Equations
@[class]
structure totally_disconnected_space (α : Type u) [topological_space α] :
Prop

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

Instances
def is_totally_separated {α : Type u} [topological_space α] :
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.