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 ≤ filter.principal s → (∃ (a : α) (H : a ∈ s), cluster_pt a f)

Instances for is_compact

topological_space.compacts.is_compact.can_lift

source

theorem is_compact.compl_mem_sets {α : Type u} [topological_space α] {s : set α} (hs : is_compact s) {f : filter α} (hf : ∀ (a : α), a ∈ s → sᶜ ∈ nhds a ⊓ f) :

sᶜ ∈ f

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

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 ∈ nhds_within a s), tᶜ ∈ f)) :

sᶜ ∈ f

The complement to a compact set belongs to a filter f if each a ∈ s has a neighborhood t within s such that tᶜ belongs to f.

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 ∈ nhds_within x s), p t)) :

p s

If p : set α → Prop is stable under restriction and union, and each point x of a compact 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 is_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 ≤ filter.principal 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 ≤ filter.principal s → (∃ (a : α) (H : a ∈ s), ↑f ≤ nhds a)

source

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

is_compact s → ∀ (f : ultrafilter α), ↑f ≤ filter.principal s → (∃ (a : α) (H : a ∈ s), ↑f ≤ nhds a)

Alias of the forward direction 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 ∈ nhds 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 ∈ nhds x) :

∃ (t : finset α), (∀ (x : α), x ∈ t → x ∈ s) ∧ s ⊆ ⋃ (x : α) (H : x ∈ t), U x

source

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

disjoint (nhds_set s) l ↔ ∀ (x : α), x ∈ s → disjoint (nhds x) l

The neighborhood filter of a compact set is disjoint with a filter l if and only if the neighborhood filter of each point of this set is disjoint with l.

source

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

disjoint l (nhds_set s) ↔ ∀ (x : α), x ∈ s → disjoint l (nhds x)

A filter l is disjoint with the neighborhood filter of a compact set if and only if it is disjoint with the neighborhood filter of each point of this set.

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 nhds (x₀, y), P z.fst z.snd)) :

∀ᶠ (x : α) in nhds 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.is_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.is_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 is_compact_accumulate {α : Type u} [topological_space α] {K : ℕ → set α} (hK : ∀ (n : ℕ), is_compact (K n)) (n : ℕ) :

is_compact (set.accumulate K n)

source

theorem is_compact_Union {α : Type u} {ι : Type u_1} [topological_space α] {f : ι → set α} [finite ι] (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 (has_insert.insert a s)

source

theorem exists_subset_nhds_of_is_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 ∈ nhds 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

theorem is_compact_open_iff_eq_finite_Union_of_is_topological_basis {α : Type u} {ι : Type u_1} [topological_space α] (b : ι → set α) (hb : topological_space.is_topological_basis (set.range b)) (hb' : ∀ (i : ι), is_compact (b i)) (U : set α) :

is_compact U ∧ is_open U ↔ ∃ (s : set ι), s.finite ∧ U = ⋃ (i : ι) (H : i ∈ s), b i

If α has a basis consisting of compact opens, then an open set in α is compact open iff it is a finite union of some elements in the basis

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), filter.principal sᶜ

Instances for filter.cocompact

filter.cocompact.filter.ne_bot

source

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

(filter.cocompact α).has_basis is_compact has_compl.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 α) (nhds b)) (hfc : continuous f) :

is_compact (has_insert.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 (nhds a)) :

is_compact (has_insert.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 (nhds a)) :

is_compact (has_insert.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), filter.principal sᶜ

Instances for filter.coclosed_compact

filter.coclosed_compact.filter.ne_bot

source

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

(filter.coclosed_compact α).has_basis (λ (s : set α), is_closed s ∧ is_compact s) has_compl.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

is_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 of this typeclass

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 is_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 ∈ nhds 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 of this typeclass

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

theorem finite_of_compact_of_discrete {α : Type u} [topological_space α] [compact_space α] [discrete_topology α] :

finite α

A compact discrete space is finite.

source

theorem exists_nhds_ne_ne_bot (α : Type u_1) [topological_space α] [compact_space α] [infinite α] :

∃ (z : α), (nhds_within z {z}ᶜ).ne_bot

source

theorem finite_cover_nhds_interior {α : Type u} [topological_space α] [compact_space α] {U : α → set α} (hU : ∀ (x : α), U x ∈ nhds 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 ∈ nhds 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_finite_univ _

source

theorem filter.comap_cocompact_le {α : 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_compact_diagonal {α : Type u} [topological_space α] [compact_space α] :

is_compact (set.diagonal α)

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_nhds_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 ∈ nhds 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 is_compact_iff_is_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.finite {α : Type u} [topological_space α] {s : set α} (hs : is_compact s) (hs' : discrete_topology ↥s) :

s.finite

source

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

∃ (z : α) (H : z ∈ s), (nhds_within z {z}ᶜ ⊓ filter.principal s).ne_bot

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 finite.compact_space {α : Type u} [topological_space α] [finite α] :

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} [finite ι] [Π (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: product of compact sets is compact.

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)

Tychonoff's theorem formulated using set.pi: product of compact sets is compact.

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)

Tychonoff's theorem formulated in terms of filters: filter.cocompact on an indexed product type Π d, κ d the filter.Coprod of filters filter.cocompact on κ d.

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 ∈ nhds x → (∃ (s : set α) (H : s ∈ nhds 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 of this typeclass

source

theorem compact_basis_nhds {α : Type u} [topological_space α] [locally_compact_space α] (x : α) :

(nhds x).has_basis (λ (s : set α), s ∈ nhds x ∧ is_compact s) (λ (s : set α), s)

source

theorem local_compact_nhds {α : Type u} [topological_space α] [locally_compact_space α] {x : α} {n : set α} (h : n ∈ nhds x) :

∃ (s : set α) (H : s ∈ nhds 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 : α), (nhds 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

@[protected, instance]

def locally_compact_space.pi_finite {ι : Type u_1} {π : ι → Type u_2} [Π (i : ι), topological_space (π i)] [∀ (i : ι), locally_compact_space (π i)] [finite ι] :

locally_compact_space (Π (i : ι), π i)

In general it suffices that all but finitely many of the spaces are compact, but that's not straightforward to state and use.

source

@[protected, instance]

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

locally_compact_space (Π (i : ι), π i)

For spaces that are not Hausdorff.

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 ∈ nhds x

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

source

theorem exists_compact_between {α : Type u} [topological_space α] [hα : locally_compact_space α] {K U : set α} (hK : is_compact K) (hU : is_open U) (h_KU : K ⊆ U) :

∃ (L : set α), is_compact L ∧ K ⊆ interior L ∧ L ⊆ U

In a locally compact space, for every containement K ⊆ U of a compact set K in an open set U, there is a compact neighborhood L such that K ⊆ L ⊆ U: equivalently, there is a compact L such that K ⊆ interior L and L ⊆ U.

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 ≤ nhds (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 of this typeclass

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 ∈ nhds_within x s) :

∃ (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 ∈ nhds 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).

Instances for compact_exhaustion

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 the forward direction 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.prod {α : Type u} {β : Type v} [topological_space α] [topological_space β] {s : set α} {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} [finite β] {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 : set β} {f : β → set α} (hs : s.finite) (h : ∀ (i : β), i ∈ s → is_clopen (f i)) :

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

source

theorem is_clopen_bUnion_finset {α : 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} [finite β] {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 : set β} (hs : s.finite) {f : β → set α} (h : ∀ (i : β), i ∈ s → is_clopen (f i)) :

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

source

theorem is_clopen_bInter_finset {α : 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.preimage {α : Type u} {β : Type v} [topological_space α] [topological_space β] {s : set β} (h : is_clopen s) {f : α → β} (hf : continuous f) :

is_clopen (f ⁻¹' s)

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

theorem continuous_bool_indicator_iff_clopen {X : Type u_3} [topological_space X] (U : set X) :

continuous U.bool_indicator ↔ is_clopen U

source

theorem continuous_on_indicator_iff_clopen {X : Type u_3} [topological_space X] (s U : set X) :

continuous_on U.bool_indicator s ↔ is_clopen (coe ⁻¹' U)

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

is_preirreducible (closure s) ↔ is_preirreducible s

source

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

is_irreducible (closure s) ↔ is_irreducible s

source

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

is_preirreducible s → is_preirreducible (closure s)

Alias of the reverse direction of is_preirreducible_iff_closure.

source

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

is_irreducible s → is_irreducible (closure s)

Alias of the reverse direction of is_irreducible_iff_closure.

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

set (set α)

The set of irreducible components of a topological space.

Equations

irreducible_components α = maximals has_le.le {s : set α | is_irreducible s}

source

theorem is_closed_of_mem_irreducible_components {α : Type u} [topological_space α] (s : set α) (H : s ∈ irreducible_components α) :

is_closed s

source

theorem irreducible_components_eq_maximals_closed (α : Type u_1) [topological_space α] :

irreducible_components α = maximals has_le.le {s : set α | is_closed s ∧ is_irreducible s}

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

irreducible_component x ∈ irreducible_components α

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 of this typeclass

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 of this typeclass

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

@[protected]

theorem is_open.dense {α : Type u} [topological_space α] [preirreducible_space α] {s : set α} (ho : is_open s) (hne : s.nonempty) :

dense s

In a (pre)irreducible space, a nonempty open set is dense.

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

@[protected, instance]

def cofinite_topology.irreducible_space {α : Type u_1} [infinite α] :

irreducible_space (cofinite_topology α)

An infinite type with cofinite topology is an irreducible topological space.

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 #