topology.subset_properties

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

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

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 is_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 is_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 is_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 is_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 is_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 is_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 is_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 is_compact_empty {α : Type u} [topological_space α] :

is_compact ∅

source

@[simp]

theorem is_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

theorem exists_subset_nhd_of_compact' {α : Type u} [topological_space α] {ι : Type u_1} [nonempty ι] {V : ι → set α} (hV : directed superset V) (hV_cpct : ∀ (i : ι), is_compact (V i)) (hV_closed : ∀ (i : ι), is_closed (V i)) {U : set α} (hU : ∀ (x : α), (x ∈ ⋂ (i : ι), V i) → U ∈ 𝓝 x) :

∃ (i : ι), V i ⊆ U

If V : ι → set α is a decreasing family of closed compact sets then any neighborhood of ⋂ i, V i contains some V i. We assume each V i is compact and closed because α is not assumed to be Hausdorff. See exists_subset_nhd_of_compact for version assuming this.

source

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

filter α

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

Equations

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

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 filter.coclosed_compact (α : Type u_1) [topological_space α] :

filter α

filter.coclosed_compact is the filter generated by complements to closed compact sets. In a Hausdorff space, this is the same as filter.cocompact.

Equations

filter.coclosed_compact α = ⨅ (s : set α) (h₁ : is_closed s) (h₂ : is_compact s), 𝓟 sᶜ

source

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

(filter.coclosed_compact α).has_basis (λ (s : set α), is_closed s ∧ is_compact s) compl

source

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

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

source

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

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

source

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

filter.cocompact α ≤ filter.coclosed_compact α

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

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)

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

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

source

@[instance]

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

compact_space α

source

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

is_compact set.univ ↔ 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.elim_nhds_subcover {α : Type u_1} [topological_space α] [compact_space α] (U : α → set α) (hU : ∀ (x : α), U x ∈ 𝓝 x) :

∃ (t : finset α), (⋃ (x : α) (H : x ∈ t), U x) = ⊤

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.is_compact {α : Type u} [topological_space α] [compact_space α] {s : set α} (h : is_closed s) :

is_compact s

source

theorem filter.cocompact_ne_bot_tfae (α : Type u_1) [topological_space α] :

[(filter.cocompact α).ne_bot, (filter.coclosed_compact α).ne_bot, ¬is_compact set.univ, ¬compact_space α].tfae

source

@[instance]

def filter.coclosed_compact.filter.ne_bot {α : Type u} [topological_space α] [(filter.cocompact α).ne_bot] :

(filter.coclosed_compact α).ne_bot

ne_bot (cocompact α) is the canonical way to say that α is not a compact space using typeclasses.

source

def fintype_of_compact_of_discrete {α : Type u} [topological_space α] [compact_space α] [discrete_topology α] :

fintype α

A compact discrete space is finite.

Equations

fintype_of_compact_of_discrete = set.fintype_of_univ_finite fintype_of_compact_of_discrete._proof_1

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

hf.fintype_of_compact hne = set.fintype_of_univ_finite _

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 is_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_is_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 exists_subset_nhd_of_compact_space {α : Type u} [topological_space α] [compact_space α] {ι : Type u_1} [nonempty ι] {V : ι → set α} (hV : directed superset V) (hV_closed : ∀ (i : ι), is_closed (V i)) {U : set α} (hU : ∀ (x : α), (x ∈ ⋂ (i : ι), V i) → U ∈ 𝓝 x) :

∃ (i : ι), V i ⊆ U

source

theorem embedding.is_compact_iff_is_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 closed_embedding.tendsto_cocompact {α : Type u} {β : Type v} [topological_space α] [topological_space β] {f : α → β} (hf : closed_embedding f) :

filter.tendsto f (filter.cocompact α) (filter.cocompact β)

A closed embedding is proper, ie, inverse images of compact sets are contained in compacts.

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 is_compact_iff_is_compact_univ {α : Type u} [topological_space α] {s : set α} :

is_compact s ↔ is_compact set.univ

source

theorem is_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 is_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 is_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

theorem filter.Coprod_cocompact {δ : Type u_1} {κ : δ → Type u_2} [Π (d : δ), topological_space (κ d)] :

filter.Coprod (λ (d : δ), filter.cocompact (κ d)) = filter.cocompact (Π (d : δ), κ d)

Product of compact sets is compact

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

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

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

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

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

compact_covering α = set.accumulate sigma_compact_space.exists_compact_covering.some

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

∃ (n : ℕ), x ∈ 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_within_of_sigma_compact {α : Type u} [topological_space α] [sigma_compact_space α] {f : α → set α} {s : set α} (hs : is_closed s) (hf : ∀ (x : α), x ∈ s → f x ∈ 𝓝[s] x) :

∃ (t : set α) (H : t ⊆ s), t.countable ∧ s ⊆ ⋃ (x : α) (H : x ∈ t), f x

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

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

to_fun : ℕ → set X
is_compact' : ∀ (n : ℕ), is_compact (self.to_fun n)
subset_interior_succ' : ∀ (n : ℕ), self.to_fun n ⊆ interior (self.to_fun (n + 1))
Union_eq' : (⋃ (n : ℕ), self.to_fun n) = set.univ

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

compact_exhaustion.has_coe_to_fun = {F := λ (x : compact_exhaustion α), ℕ → set α, coe := compact_exhaustion.to_fun _inst_1}

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

K.find x = nat.find _

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

K.shiftr = {to_fun := λ (n : ℕ), n.cases_on ∅ ⇑K, is_compact' := _, subset_interior_succ' := _, Union_eq' := _}

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

compact_exhaustion.choice X = classical.choice _

source

@[instance]

def compact_exhaustion.inhabited {α : Type u} [topological_space α] [locally_compact_space α] [sigma_compact_space α] :

inhabited (compact_exhaustion α)

Equations

compact_exhaustion.inhabited = {default := compact_exhaustion.choice α _inst_3}

source

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)

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_Union {α : 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_bUnion {α : 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 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

@[simp]

theorem is_clopen_discrete {α : Type u} [topological_space α] [discrete_topology α] (x : set α) :

is_clopen x

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

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

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

is_irreducible s = (s.nonempty ∧ is_preirreducible s)

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

irreducible_component x = classical.some _

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

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

source

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

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.

mathlib documentation

Properties of subsets of topological spaces #

Main definitions #

On the definition of irreducible and connected sets/spaces #