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:

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

Furthermore, we have two more classes:

On the definition of irreducible and connected sets/spaces #

In informal mathematics, irreducible spaces are assumed to be nonempty. We formalise the predicate without that assumption as is_preirreducible. In other words, the only difference is whether the empty space counts as irreducible. 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 nontrivial filter f that contains s, there exists a ∈ s such that every set of f meets every neighborhood of a.

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 set s has a neighborhood t within s such that p t, then p 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 : ultrafilter α), ↑f ≤ 𝓟 s → (∃ (a : α) (H : a ∈ s), ↑f ≤ 𝓝 a)
source
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.

source
theorem is_compact.elim_directed_cover {α : Type u} [topological_space α] {s : set α} {ι : Type v} [hι : nonempty ι] (hs : is_compact s) (U : ι → set α) (hUo : ∀ (i : ι), is_open (U i)) (hsU : s ⊆ ⋃ (i : ι), U i) (hdU : directed has_subset.subset U) :
∃ (i : ι), s ⊆ U i

For every open directed cover of a compact set, there exists a single element of the cover which itself includes the set.

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_nhds_subcover' {α : Type u} [topological_space α] {s : set α} (hs : is_compact s) (U : Π (x : α), x ∈ s → set α) (hU : ∀ (x : α) (H : x ∈ s), U x H ∈ 𝓝 x) :
∃ (t : finset ↥s), s ⊆ ⋃ (x : ↥s) (H : x ∈ t), U ↑x _
source
theorem is_compact.elim_nhds_subcover {α : Type u} [topological_space α] {s : set α} (hs : is_compact s) (U : α → set α) (hU : ∀ (x : α), x ∈ s → U x ∈ 𝓝 x) :
∃ (t : finset α), (∀ (x : α), x ∈ t → x ∈ s) ∧ s ⊆ ⋃ (x : α) (H : x ∈ t), U x
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 locally_finite.finite_nonempty_inter_compact {α : Type u} [topological_space α] {ι : Type u_1} {f : ι → set α} (hf : locally_finite f) {s : set α} (hs : is_compact s) :
{i : ι | (f i ∩ s).nonempty}.finite

If s is a compact set in a topological space α and f : ι → set α is a locally finite family of sets, then f i ∩ s is nonempty only for a finitely many i.

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.subsingleton.is_compact {α : Type u} [topological_space α] {s : set α} (hs : s.subsingleton) :
is_compact s
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 finset.compact_bUnion {α : Type u} {β : Type v} [topological_space α] (s : finset β) {f : β → set α} (hf : ∀ (i : β), i ∈ s → is_compact (f i)) :
is_compact (⋃ (i : β) (H : i ∈ s), f i)
source
theorem compact_accumulate {α : Type u} [topological_space α] {K : ℕ → set α} (hK : ∀ (n : ℕ), is_compact (K n)) (n : ℕ) :
is_compact (set.accumulate K n)
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 finite_of_is_compact_of_discrete {α : Type u} [topological_space α] [discrete_topology α] (s : set α) (hs : is_compact s) :
s.finite
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
theorem is_compact.insert {α : Type u} [topological_space α] {s : set α} (hs : is_compact s) (a : α) :
is_compact (insert a s)
source
def filter.cocompact (α : Type u_1) [topological_space α] :
filter α

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

Equations
source
theorem filter.has_basis_cocompact {α : Type u} [topological_space α] :
(filter.cocompact α).has_basis is_compact compl
source
theorem filter.mem_cocompact {α : Type u} [topological_space α] {s : set α} :
s ∈ filter.cocompact α ↔ ∃ (t : set α), is_compact t ∧ tᶜ ⊆ s
source
theorem filter.mem_cocompact' {α : Type u} [topological_space α] {s : set α} :
s ∈ filter.cocompact α ↔ ∃ (t : set α), is_compact t ∧ sᶜ ⊆ t
source
theorem is_compact.compl_mem_cocompact {α : Type u} [topological_space α] {s : set α} (hs : is_compact s) :
sᶜ ∈ filter.cocompact α
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 β} :
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

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.

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
@[instance]
def subsingleton.compact_space {α : Type u} [topological_space α] [subsingleton α] :
compact_space α
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
def fintype_of_compact_of_discrete {α : Type u} [topological_space α] [compact_space α] [discrete_topology α] :
fintype α

A compact discrete space is finite.

Equations
source
theorem finite_cover_nhds_interior {α : Type u} [topological_space α] [compact_space α] {U : α → set α} (hU : ∀ (x : α), U x ∈ 𝓝 x) :
∃ (t : finset α), (⋃ (x : α) (H : x ∈ t), interior (U x)) = set.univ
source
theorem finite_cover_nhds {α : Type u} [topological_space α] [compact_space α] {U : α → set α} (hU : ∀ (x : α), U x ∈ 𝓝 x) :
∃ (t : finset α), (⋃ (x : α) (H : x ∈ t), U x) = set.univ
source
theorem locally_finite.finite_nonempty_of_compact {α : Type u} [topological_space α] {ι : Type u_1} [compact_space α] {f : ι → set α} (hf : locally_finite f) :
{i : ι | (f i).nonempty}.finite

If α is a compact space, then a locally finite family of sets of α can have only finitely many nonempty elements.

source
theorem locally_finite.finite_of_compact {α : Type u} [topological_space α] {ι : Type u_1} [compact_space α] {f : ι → set α} (hf : locally_finite f) (hne : ∀ (i : ι), (f i).nonempty) :
set.univ.finite

If α is a compact space, then a locally finite family of nonempty sets of α can have only finitely many elements, set.finite version.

source
def locally_finite.fintype_of_compact {α : Type u} [topological_space α] {ι : Type u_1} [compact_space α] {f : ι → set α} (hf : locally_finite f) (hne : ∀ (i : ι), (f i).nonempty) :
fintype ι

If α is a compact space, then a locally finite family of nonempty sets of α can have only finitely many elements, fintype version.

Equations
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
theorem inducing.is_compact_iff {α : Type u} {β : Type v} [topological_space α] [topological_space β] {f : α → β} (hf : inducing f) {s : set α} :
is_compact (f '' s) ↔ is_compact s
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 filter.coprod_cocompact {α : Type u} [topological_space α] {β : Type u_1} [topological_space β] :
(filter.cocompact α).coprod (filter.cocompact β) = filter.cocompact (α × β)

The coproduct of the cocompact filters on two topological spaces is the cocompact filter on their product.

source
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

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_space {ι : 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 compact_basis_nhds {α : Type u} [topological_space α] [locally_compact_space α] (x : α) :
(𝓝 x).has_basis (λ (s : set α), s ∈ 𝓝 x ∧ is_compact s) (λ (s : set α), s)
source
theorem locally_compact_space_of_has_basis {α : Type u} [topological_space α] {ι : α → Type u_1} {p : Π (x : α), ι x → Prop} {s : Π (x : α), ι x → set α} (h : ∀ (x : α), (𝓝 x).has_basis (p x) (s x)) (hc : ∀ (x : α) (i : ι x), p x i → is_compact (s x i)) :
locally_compact_space α
source
@[instance]
def locally_compact_space.prod (α : Type u_1) (β : Type u_2) [topological_space α] [topological_space β] [locally_compact_space α] [locally_compact_space β] :
locally_compact_space (α × β)
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
theorem exists_compact_mem_nhds {α : Type u} [topological_space α] [locally_compact_space α] (x : α) :
∃ (K : set α), is_compact K ∧ K ∈ 𝓝 x

In a locally compact space every point has a compact neighborhood.

source
theorem exists_compact_superset {α : Type u} [topological_space α] [locally_compact_space α] {K : set α} (hK : is_compact K) :
∃ (K' : set α), is_compact K' ∧ K ⊆ interior K'

In a locally compact space, every compact set is contained in the interior of a compact set.

source
theorem ultrafilter.le_nhds_Lim {α : Type u} [topological_space α] [compact_space α] (F : ultrafilter α) :
↑F ≤ 𝓝 (Lim ↑F)
source
theorem is_closed.exists_minimal_nonempty_closed_subset {α : Type u} [topological_space α] [compact_space α] {S : set α} (hS : is_closed S) (hne : S.nonempty) :
∃ (V : set α), V ⊆ S ∧ V.nonempty ∧ is_closed V ∧ ∀ (V' : set α), V' ⊆ V → V'.nonempty → is_closed V' → V' = V
source
@[class]
structure sigma_compact_space (α : Type u_1) [topological_space α] :
Prop

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
source
@[instance]
def compact_space.sigma_compact {α : Type u} [topological_space α] [compact_space α] :
sigma_compact_space α
source
theorem sigma_compact_space.of_countable {α : Type u} [topological_space α] (S : set (set α)) (Hc : S.countable) (Hcomp : ∀ (s : set α), s ∈ S → is_compact s) (HU : ⋃₀S = set.univ) :
sigma_compact_space α
source
@[instance]
def sigma_compact_space_of_locally_compact_second_countable {α : Type u} [topological_space α] [locally_compact_space α] [topological_space.second_countable_topology α] :
sigma_compact_space α
source
def compact_covering (α : Type u) [topological_space α] [sigma_compact_space α] :
ℕ → set α

A choice of compact covering for a σ-compact space, chosen to be monotone.

Equations
source
theorem is_compact_compact_covering (α : Type u) [topological_space α] [sigma_compact_space α] (n : ℕ) :
is_compact (compact_covering α n)
source
theorem Union_compact_covering (α : Type u) [topological_space α] [sigma_compact_space α] :
(⋃ (n : ℕ), compact_covering α n) = set.univ
source
theorem compact_covering_subset (α : Type u) [topological_space α] [sigma_compact_space α] ⦃m n : ℕ⦄ (h : m ≤ n) :
compact_covering α m ⊆ compact_covering α n
source
theorem locally_finite.countable_of_sigma_compact {α : Type u} [topological_space α] [sigma_compact_space α] {ι : Type u_1} {f : ι → set α} (hf : locally_finite f) (hne : ∀ (i : ι), (f i).nonempty) :
set.univ.countable

If α is a σ-compact space, then a locally finite family of nonempty sets of α can have only countably many elements, set.countable version.

source
theorem countable_cover_nhds_of_sigma_compact {α : Type u} [topological_space α] [sigma_compact_space α] {f : α → set α} (hf : ∀ (x : α), f x ∈ 𝓝 x) :
∃ (s : set α), s.countable ∧ (⋃ (x : α) (H : x ∈ s), f x) = set.univ

In a topological space with sigma compact topology, if f is a function that sends each point x to a neighborhood of x, then for some countable set s, the neighborhoods f x, x ∈ s, cover the whole space.

source
structure compact_exhaustion (X : Type u_1) [topological_space X] :
Type u_1

An exhaustion by compact sets of a topological space is a sequence of compact sets K n such that K n ⊆ interior (K (n + 1)) and (⋃ n, K n) = univ.

If X is a locally compact sigma compact space, then compact_exhaustion.choice X provides a choice of an exhaustion by compact sets. This choice is also available as (default : compact_exhaustion X).

source
@[instance]
def compact_exhaustion.has_coe_to_fun {α : Type u} [topological_space α] :
has_coe_to_fun (compact_exhaustion α)
Equations
source
theorem compact_exhaustion.is_compact {α : Type u} [topological_space α] (K : compact_exhaustion α) (n : ℕ) :
is_compact (⇑K n)
source
theorem compact_exhaustion.subset_interior_succ {α : Type u} [topological_space α] (K : compact_exhaustion α) (n : ℕ) :
⇑K n ⊆ interior (⇑K (n + 1))
source
theorem compact_exhaustion.subset_succ {α : Type u} [topological_space α] (K : compact_exhaustion α) (n : ℕ) :
⇑K n ⊆ ⇑K (n + 1)
source
theorem compact_exhaustion.subset {α : Type u} [topological_space α] (K : compact_exhaustion α) ⦃m n : ℕ⦄ (h : m ≤ n) :
⇑K m ⊆ ⇑K n
source
theorem compact_exhaustion.subset_interior {α : Type u} [topological_space α] (K : compact_exhaustion α) ⦃m n : ℕ⦄ (h : m < n) :
⇑K m ⊆ interior (⇑K n)
source
theorem compact_exhaustion.Union_eq {α : Type u} [topological_space α] (K : compact_exhaustion α) :
(⋃ (n : ℕ), ⇑K n) = set.univ
source
theorem compact_exhaustion.exists_mem {α : Type u} [topological_space α] (K : compact_exhaustion α) (x : α) :
∃ (n : ℕ), x ∈ ⇑K n
source
def compact_exhaustion.find {α : Type u} [topological_space α] (K : compact_exhaustion α) (x : α) :
ℕ

The minimal n such that x ∈ K n.

Equations
source
theorem compact_exhaustion.mem_find {α : Type u} [topological_space α] (K : compact_exhaustion α) (x : α) :
x ∈ ⇑K (K.find x)
source
theorem compact_exhaustion.mem_iff_find_le {α : Type u} [topological_space α] (K : compact_exhaustion α) {x : α} {n : ℕ} :
x ∈ ⇑K n ↔ K.find x ≤ n
source
def compact_exhaustion.shiftr {α : Type u} [topological_space α] (K : compact_exhaustion α) :
compact_exhaustion α

Prepend the empty set to a compact exhaustion K n.

Equations
source
@[simp]
theorem compact_exhaustion.find_shiftr {α : Type u} [topological_space α] (K : compact_exhaustion α) (x : α) :
K.shiftr.find x = K.find x + 1
source
theorem compact_exhaustion.mem_diff_shiftr_find {α : Type u} [topological_space α] (K : compact_exhaustion α) (x : α) :
x ∈ ⇑(K.shiftr) (K.find x + 1) \ ⇑(K.shiftr) (K.find x)
source
def compact_exhaustion.choice (X : Type u_1) [topological_space X] [locally_compact_space X] [sigma_compact_space X] :
compact_exhaustion X

A choice of an exhaustion by compact sets of a locally compact sigma compact space.

Equations
source
@[instance]
def compact_exhaustion.inhabited {α : Type u} [topological_space α] [locally_compact_space α] [sigma_compact_space α] :
inhabited (compact_exhaustion α)
Equations
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
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)
source
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)
source
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)
source
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.

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 α} :
is_preirreducible s → 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 α} :
is_open s → is_open t → s.nonempty → 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.