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_3 : 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.image_of_continuous_on {α : Type u} {β : Type v} [topological_space α] [topological_space β] {s : set α} {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 α] [topological_space β] {s : set α} {f : α → β} (hs : is_compact s) (hf : continuous f) :

is_compact (f '' s)

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 u_1} [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

theorem is_compact.eventually_forall_of_forall_eventually {α : Type u} {β : Type v} [topological_space α] [topological_space β] {x₀ : α} {K : set β} (hK : is_compact K) {P : α → β → Prop} (hP : ∀ (y : β), y ∈ K → (∀ᶠ (z : α × β) in 𝓝 (x₀, y), P z.fst z.snd)) :

∀ᶠ (x : α) in 𝓝 x₀, ∀ (y : β), y ∈ K → P x y

To show that ∀ y ∈ K, P x y holds for x close enough to x₀ when K is compact, it is sufficient to show that for all y₀ ∈ K there P x y holds for (x, y) close enough to (x₀, y₀).

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 u_1} [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 u_1} [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 u_1} [topological_space α] {f : ι → set α} [fintype ι] (h : ∀ (i : ι), is_compact (f i)) :

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

source

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

is_compact s

source

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

s.finite

source

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

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

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

filter.cocompact α ≤ filter.cofinite

source

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

filter.cocompact α = filter.cofinite

source

@[simp]

theorem nat.cocompact_eq :

filter.cocompact ℕ = filter.at_top

source

theorem filter.tendsto.is_compact_insert_range_of_cocompact {α : Type u} {β : Type v} [topological_space α] [topological_space β] {f : α → β} {b : β} (hf : filter.tendsto f (filter.cocompact α) (𝓝 b)) (hfc : continuous f) :

is_compact (insert b (set.range f))

source

theorem filter.tendsto.is_compact_insert_range_of_cofinite {α : Type u} {ι : Type u_1} [topological_space α] {f : ι → α} {a : α} (hf : filter.tendsto f filter.cofinite (𝓝 a)) :

is_compact (insert a (set.range f))

source

theorem filter.tendsto.is_compact_insert_range {α : Type u} [topological_space α] {f : ℕ → α} {a : α} (hf : filter.tendsto f filter.at_top (𝓝 a)) :

is_compact (insert a (set.range f))

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

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

sᶜ ∈ filter.coclosed_compact α

source

def bornology.in_compact (α : Type u) [topological_space α] :

bornology α

Sets that are contained in a compact set form a bornology. Its cobounded filter is filter.cocompact. See also bornology.relatively_compact the bornology of sets with compact closure.

Equations

bornology.in_compact α = {cobounded := filter.cocompact α _inst_1, le_cofinite := _}

source

theorem bornology.in_compact.is_bounded_iff {α : Type u} [topological_space α] {s : set α} :

bornology.is_bounded s ↔ ∃ (t : set α), is_compact t ∧ s ⊆ t

source

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

Prop

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

Equations

nhds_contain_boxes s t = ∀ (n : set (α × β)), is_open n → s ×ˢ t ⊆ n → (∃ (u : set α) (v : set β), is_open u ∧ is_open v ∧ s ⊆ u ∧ t ⊆ v ∧ u ×ˢ 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 ×ˢ t ⊆ n) :

∃ (u : set α) (v : set β), is_open u ∧ is_open v ∧ s ⊆ u ∧ t ⊆ v ∧ u ×ˢ 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_3) [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

@[protected, 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} [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

@[class]

structure noncompact_space (α : Type u_3) [topological_space α] :

Prop

noncompact_univ : ¬is_compact set.univ

α is a noncompact topological space if it not a compact space.

Instances

source

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

s ≠ set.univ

source

@[protected, instance]

def filter.cocompact.filter.ne_bot {α : Type u} [topological_space α] [noncompact_space α] :

(filter.cocompact α).ne_bot

source

@[simp]

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

filter.cocompact α = ⊥

source

@[protected, instance]

def filter.coclosed_compact.filter.ne_bot {α : Type u} [topological_space α] [noncompact_space α] :

(filter.coclosed_compact α).ne_bot

source

theorem noncompact_space_of_ne_bot {α : Type u} [topological_space α] (h : (filter.cocompact α).ne_bot) :

noncompact_space α

source

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

(filter.cocompact α).ne_bot ↔ noncompact_space α

source

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

¬compact_space α ↔ noncompact_space α

source

@[protected, instance]

def int.noncompact_space :

noncompact_space ℤ

source

noncomputable 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

noncomputable 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 filter.comap_cocompact {α : Type u} {β : Type v} [topological_space α] [topological_space β] {f : α → β} (hf : continuous f) :

filter.comap f (filter.cocompact β) ≤ filter.cocompact α

The comap of the cocompact filter on β by a continuous function f : α → β is less than or equal to the cocompact filter on α. This is a reformulation of the fact that images of compact sets are compact.

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

If f : α → β is an inducing map, then the image f '' s of a set s is compact if and only if the set s is closed.

source

theorem embedding.is_compact_iff_is_compact_image {α : Type u} {β : Type v} [topological_space α] [topological_space β] {s : set α} {f : α → β} (hf : embedding f) :

is_compact s ↔ is_compact (f '' s)

If f : α → β is an embedding (or more generally, an inducing map, see inducing.is_compact_iff), then the image f '' s of a set s is compact if and only if the set s is closed.

source

theorem closed_embedding.is_compact_preimage {α : Type u} {β : Type v} [topological_space α] [topological_space β] {f : α → β} (hf : closed_embedding f) {K : set β} (hK : is_compact K) :

is_compact (f ⁻¹' K)

The preimage of a compact set under a closed embedding is a compact set.

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. Moreover, the preimage of a compact set is compact, see closed_embedding.is_compact_preimage.

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

@[protected]

theorem closed_embedding.noncompact_space {α : Type u} {β : Type v} [topological_space α] [topological_space β] [noncompact_space α] {f : α → β} (hf : closed_embedding f) :

noncompact_space β

source

@[protected]

theorem closed_embedding.compact_space {α : Type u} {β : Type v} [topological_space α] [topological_space β] [h : compact_space β] {f : α → β} (hf : closed_embedding f) :

compact_space α

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 ×ˢ t)

source

@[protected, instance]

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

compact_space α

Finite topological spaces are compact.

source

@[protected, 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

@[protected, 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

@[protected, instance]

def sigma.compact_space {ι : Type u_1} {π : ι → Type u_2} [fintype ι] [Π (i : ι), topological_space (π i)] [∀ (i : ι), compact_space (π i)] :

compact_space (Σ (i : ι), π i)

source

theorem filter.coprod_cocompact {α : Type u} {β : Type v} [topological_space α] [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 prod.noncompact_space_iff {α : Type u} {β : Type v} [topological_space α] [topological_space β] :

noncompact_space (α × β) ↔ noncompact_space α ∧ nonempty β ∨ nonempty α ∧ noncompact_space β

source

@[protected, instance]

def prod.noncompact_space_left {α : Type u} {β : Type v} [topological_space α] [topological_space β] [noncompact_space α] [nonempty β] :

noncompact_space (α × β)

source

@[protected, instance]

def prod.noncompact_space_right {α : Type u} {β : Type v} [topological_space α] [topological_space β] [nonempty α] [noncompact_space β] :

noncompact_space (α × β)

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

@[protected, 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

@[protected, instance]

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

compact_space (quot r)

source

@[protected, 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_3) [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 local_compact_nhds {α : Type u} [topological_space α] [locally_compact_space α] {x : α} {n : set α} (h : n ∈ 𝓝 x) :

∃ (s : set α) (H : s ∈ 𝓝 x), s ⊆ n ∧ is_compact 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

@[protected, 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

@[protected]

theorem closed_embedding.locally_compact_space {α : Type u} {β : Type v} [topological_space α] [topological_space β] [locally_compact_space β] {f : α → β} (hf : closed_embedding f) :

locally_compact_space α

source

@[protected]

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

locally_compact_space ↥s

source

@[protected]

theorem open_embedding.locally_compact_space {α : Type u} {β : Type v} [topological_space α] [topological_space β] [locally_compact_space β] {f : α → β} (hf : open_embedding f) :

locally_compact_space α

source

@[protected]

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

locally_compact_space ↥s

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

@[protected, 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

@[protected, 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

@[protected]

theorem locally_finite.countable_univ {α : 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

@[protected]

noncomputable def locally_finite.encodable {α : Type u} [topological_space α] [sigma_compact_space α] {ι : Type u_1} {f : ι → set α} (hf : locally_finite f) (hne : ∀ (i : ι), (f i).nonempty) :

encodable ι

If f : ι → set α is a locally finite covering of a σ-compact topological space by nonempty sets, then the index type ι is encodable.

Equations

hf.encodable hne = encodable.of_equiv ↥set.univ (equiv.set.univ ι).symm

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_3) [topological_space X] :

Type u_3

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

@[protected, instance]

def compact_exhaustion.has_coe_to_fun {α : Type u} [topological_space α] :

has_coe_to_fun (compact_exhaustion α) (λ (_x : compact_exhaustion α), ℕ → set α)

Equations

compact_exhaustion.has_coe_to_fun = {coe := compact_exhaustion.to_fun _inst_1}

source

@[protected]

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

@[protected]

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

@[protected]

noncomputable 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

noncomputable 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

@[protected, instance]

noncomputable 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_4}

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

@[protected]

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

is_open s

source

@[protected]

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

is_closed s

source

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

is_clopen s ↔ frontier s = ∅

source

theorem is_clopen.frontier_eq {α : Type u} [topological_space α] {s : set α} :

is_clopen s → frontier s = ∅

Alias of is_clopen_iff_frontier_eq_empty.

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} {β : Type v} [topological_space α] [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

theorem clopen_range_sigma_mk {ι : Type u_1} {σ : ι → Type u_2} [Π (i : ι), topological_space (σ i)] {i : ι} :

is_clopen (set.range (sigma.mk i))

source

@[protected]

theorem quotient_map.is_clopen_preimage {α : Type u} {β : Type v} [topological_space α] [topological_space β] {f : α → β} (hf : quotient_map f) {s : set β} :

is_clopen (f ⁻¹' s) ↔ is_clopen s

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 set.subsingleton.is_preirreducible {α : Type u} [topological_space α] {s : set α} (hs : s.subsingleton) :

is_preirreducible s

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.

Instances

prime_spectrum.irreducible_space

source

theorem irreducible_space.is_irreducible_univ (α : Type u) [topological_space α] [irreducible_space α] :

is_irreducible ⊤

source

theorem irreducible_space_def (α : Type u) [topological_space α] :

irreducible_space α ↔ is_irreducible ⊤

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.

source

theorem subset_closure_inter_of_is_preirreducible_of_is_open {α : Type u} [topological_space α] {S U : set α} (hS : is_preirreducible S) (hU : is_open U) (h : (S ∩ U).nonempty) :

S ⊆ closure (S ∩ U)

A nonemtpy open subset of a preirreducible subspace is dense in the subspace.

source

theorem is_preirreducible.subset_irreducible {α : Type u} [topological_space α] {S U Z : set α} (hZ : is_preirreducible Z) (hU : U.nonempty) (hU' : is_open U) (h₁ : U ⊆ S) (h₂ : S ⊆ Z) :

is_irreducible S

If ∅ ≠ U ⊆ S ⊆ Z such that U is open and Z is preirreducible, then S is irreducible.

source

theorem is_preirreducible.open_subset {α : Type u} [topological_space α] {Z U : set α} (hZ : is_preirreducible Z) (hU : is_open U) (hU' : U ⊆ Z) :

is_preirreducible U

source

theorem is_preirreducible.interior {α : Type u} [topological_space α] {Z : set α} (hZ : is_preirreducible Z) :

is_preirreducible (interior Z)

source

theorem is_preirreducible.preimage {α : Type u} {β : Type v} [topological_space α] [topological_space β] {Z : set α} (hZ : is_preirreducible Z) {f : β → α} (hf : open_embedding f) :

is_preirreducible (f ⁻¹' Z)

mathlib documentation

Properties of subsets of topological spaces #

Main definitions #

On the definition of irreducible and connected sets/spaces #