Properties of subsets of topological spaces

In this file we define various properties of subsets of a topological space, and some classes on topological spaces.

Main definitions

We define the following properties for sets in a topological space:

• IsCompact: each open cover has a finite subcover. This is defined in mathlib using filters. The main property of a compact set is IsCompact.elim_finite_subcover.
• IsClopen: a set that is both open and closed.
• IsIrreducible: a nonempty set that has contains no non-trivial pair of disjoint opens. See also the section below in the module doc.

For each of these definitions (except for IsClopen), we also have a class stating that the whole space satisfies that property: CompactSpace, PreirreducibleSpace, IrreducibleSpace.

Furthermore, we have four more classes:

• WeaklyLocallyCompactSpace: every point x has a compact neighborhood.
• LocallyCompactSpace: for every point x, every open neighborhood of x contains a compact neighborhood of x. The definition is formulated in terms of the neighborhood filter.
• SigmaCompactSpace: a space that is the union of a countably many compact subspaces;
• NoncompactSpace: a space that is not a compact space.

On the definition of irreducible and connected sets/spaces

In informal mathematics, irreducible spaces are assumed to be nonempty. We formalise the predicate without that assumption as IsPreirreducible. In other words, the only difference is whether the empty space counts as irreducible. There are good reasons to consider the empty space to be “too simple to be simple” See also https://ncatlab.org/nlab/show/too+simple+to+be+simple, and in particular https://ncatlab.org/nlab/show/too+simple+to+be+simple#relationship_to_biased_definitions.

def IsCompact {α : Type u} [TopologicalSpace α] (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

• IsCompact s = ∀ ⦃f : Filter α⦄ [inst : Filter.NeBot f], f ≤ Filter.principal s → ∃ a, a ∈ s ∧ ClusterPt a f

theorem IsCompact.compl_mem_sets {α : Type u} [TopologicalSpace α] {s : Set α} (hs : IsCompact 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.

theorem IsCompact.compl_mem_sets_of_nhdsWithin {α : Type u} [TopologicalSpace α] {s : Set α} (hs : IsCompact s) {f : Filter α} (hf : ∀ (a : α), a ∈ s → ∃ t, t ∈ nhdsWithin a s ∧ tᶜ ∈ f) : sᶜ ∈ f

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

theorem IsCompact.induction_on {α : Type u} [TopologicalSpace α] {s : Set α} (hs : IsCompact 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, t ∈ nhdsWithin 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.

theorem IsCompact.inter_right {α : Type u} [TopologicalSpace α] {s : Set α} {t : Set α} (hs : IsCompact s) (ht : IsClosed t) : IsCompact (s ∩ t)

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

theorem IsCompact.inter_left {α : Type u} [TopologicalSpace α] {s : Set α} {t : Set α} (ht : IsCompact t) (hs : IsClosed s) : IsCompact (s ∩ t)

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

theorem IsCompact.diff {α : Type u} [TopologicalSpace α] {s : Set α} {t : Set α} (hs : IsCompact s) (ht : IsOpen t) : IsCompact (s \ t)

The set difference of a compact set and an open set is a compact set.

theorem IsCompact.of_isClosed_subset {α : Type u} [TopologicalSpace α] {s : Set α} {t : Set α} (hs : IsCompact s) (ht : IsClosed t) (h : t ⊆ s) : IsCompact t

A closed subset of a compact set is a compact set.

theorem IsCompact.image_of_continuousOn {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] {s : Set α} {f : α → β} (hs : IsCompact s) (hf : ContinuousOn f s) : IsCompact (f '' s)

theorem IsCompact.image {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] {s : Set α} {f : α → β} (hs : IsCompact s) (hf : Continuous f) : IsCompact (f '' s)

theorem IsCompact.adherence_nhdset {α : Type u} [TopologicalSpace α] {s : Set α} {t : Set α} {f : Filter α} (hs : IsCompact s) (hf₂ : f ≤ Filter.principal s) (ht₁ : IsOpen t) (ht₂ : ∀ (a : α), a ∈ s → ClusterPt a f → a ∈ t) : t ∈ f

theorem isCompact_iff_ultrafilter_le_nhds {α : Type u} [TopologicalSpace α] {s : Set α} : IsCompact s ↔ ∀ (f : Ultrafilter α), ↑f ≤ Filter.principal s → ∃ a, a ∈ s ∧ ↑f ≤ nhds a

theorem IsCompact.ultrafilter_le_nhds {α : Type u} [TopologicalSpace α] {s : Set α} : IsCompact s → ∀ (f : Ultrafilter α), ↑f ≤ Filter.principal s → ∃ a, a ∈ s ∧ ↑f ≤ nhds a

Alias of the forward direction of isCompact_iff_ultrafilter_le_nhds.

theorem IsCompact.elim_directed_cover {α : Type u} [TopologicalSpace α] {s : Set α} {ι : Type v} [hι : Nonempty ι] (hs : IsCompact s) (U : ι → Set α) (hUo : ∀ (i : ι), IsOpen (U i)) (hsU : s ⊆ ⋃ (i : ι), U i) (hdU : Directed (fun x x_1 => x ⊆ x_1) 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.

theorem IsCompact.elim_finite_subcover {α : Type u} [TopologicalSpace α] {s : Set α} {ι : Type v} (hs : IsCompact s) (U : ι → Set α) (hUo : ∀ (i : ι), IsOpen (U i)) (hsU : s ⊆ ⋃ (i : ι), U i) : ∃ t, s ⊆ ⋃ (i : ι) (_ : i ∈ t), U i

For every open cover of a compact set, there exists a finite subcover.

theorem IsCompact.elim_nhds_subcover' {α : Type u} [TopologicalSpace α] {s : Set α} (hs : IsCompact s) (U : (x : α) → x ∈ s → Set α) (hU : ∀ (x : α) (hx : x ∈ s), U x hx ∈ nhds x) : ∃ t, s ⊆ ⋃ (x : ↑s) (_ : x ∈ t), U ↑x (_ : ↑x ∈ s)

theorem IsCompact.elim_nhds_subcover {α : Type u} [TopologicalSpace α] {s : Set α} (hs : IsCompact s) (U : α → Set α) (hU : ∀ (x : α), x ∈ s → U x ∈ nhds x) : ∃ t, (∀ (x : α), x ∈ t → x ∈ s) ∧ s ⊆ ⋃ (x : α) (_ : x ∈ t), U x

theorem IsCompact.disjoint_nhdsSet_left {α : Type u} [TopologicalSpace α] {s : Set α} {l : Filter α} (hs : IsCompact s) : Disjoint (nhdsSet 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.

theorem IsCompact.disjoint_nhdsSet_right {α : Type u} [TopologicalSpace α] {s : Set α} {l : Filter α} (hs : IsCompact s) : Disjoint l (nhdsSet 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.

theorem IsCompact.elim_directed_family_closed {α : Type u} [TopologicalSpace α] {s : Set α} {ι : Type v} [hι : Nonempty ι] (hs : IsCompact s) (Z : ι → Set α) (hZc : ∀ (i : ι), IsClosed (Z i)) (hsZ : s ∩ ⋂ (i : ι), Z i = ∅) (hdZ : Directed (fun x x_1 => x ⊇ x_1) Z) : ∃ i, s ∩ Z i = ∅

For every directed family of closed sets whose intersection avoids a compact set, there exists a single element of the family which itself avoids this compact set.

theorem IsCompact.elim_finite_subfamily_closed {α : Type u} [TopologicalSpace α] {s : Set α} {ι : Type v} (hs : IsCompact s) (Z : ι → Set α) (hZc : ∀ (i : ι), IsClosed (Z i)) (hsZ : s ∩ ⋂ (i : ι), Z i = ∅) : ∃ t, s ∩ ⋂ (i : ι) (_ : i ∈ t), Z i = ∅

For every family of closed sets whose intersection avoids a compact set, there exists a finite subfamily whose intersection avoids this compact set.

theorem LocallyFinite.finite_nonempty_inter_compact {α : Type u} [TopologicalSpace α] {ι : Type u_3} {f : ι → Set α} (hf : LocallyFinite f) {s : Set α} (hs : IsCompact s) : Set.Finite {i | Set.Nonempty (f i ∩ s)}

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.

theorem IsCompact.inter_iInter_nonempty {α : Type u} [TopologicalSpace α] {s : Set α} {ι : Type v} (hs : IsCompact s) (Z : ι → Set α) (hZc : ∀ (i : ι), IsClosed (Z i)) (hsZ : ∀ (t : Finset ι), Set.Nonempty (s ∩ ⋂ (i : ι) (_ : i ∈ t), Z i)) : Set.Nonempty (s ∩ ⋂ (i : ι), Z i)

To show that a compact set intersects the intersection of a family of closed sets, it is sufficient to show that it intersects every finite subfamily.

theorem IsCompact.nonempty_iInter_of_directed_nonempty_compact_closed {α : Type u} [TopologicalSpace α] {ι : Type v} [hι : Nonempty ι] (Z : ι → Set α) (hZd : Directed (fun x x_1 => x ⊇ x_1) Z) (hZn : ∀ (i : ι), Set.Nonempty (Z i)) (hZc : ∀ (i : ι), IsCompact (Z i)) (hZcl : ∀ (i : ι), IsClosed (Z i)) : Set.Nonempty (⋂ (i : ι), Z i)

Cantor's intersection theorem: the intersection of a directed family of nonempty compact closed sets is nonempty.

theorem IsCompact.nonempty_iInter_of_sequence_nonempty_compact_closed {α : Type u} [TopologicalSpace α] (Z : ℕ → Set α) (hZd : ∀ (i : ℕ), Z (i + 1) ⊆ Z i) (hZn : ∀ (i : ℕ), Set.Nonempty (Z i)) (hZ0 : IsCompact (Z 0)) (hZcl : ∀ (i : ℕ), IsClosed (Z i)) : Set.Nonempty (⋂ (i : ℕ), Z i)

Cantor's intersection theorem for sequences indexed by ℕ: the intersection of a decreasing sequence of nonempty compact closed sets is nonempty.

theorem IsCompact.elim_finite_subcover_image {α : Type u} {ι : Type u_1} [TopologicalSpace α] {s : Set α} {b : Set ι} {c : ι → Set α} (hs : IsCompact s) (hc₁ : ∀ (i : ι), i ∈ b → IsOpen (c i)) (hc₂ : s ⊆ ⋃ (i : ι) (_ : i ∈ b), c i) : ∃ b', b' ⊆ b ∧ Set.Finite b' ∧ s ⊆ ⋃ (i : ι) (_ : i ∈ b'), c i

For every open cover of a compact set, there exists a finite subcover.

theorem isCompact_of_finite_subcover {α : Type u} [TopologicalSpace α] {s : Set α} (h : ∀ {ι : Type u} (U : ι → Set α), (∀ (i : ι), IsOpen (U i)) → s ⊆ ⋃ (i : ι), U i → ∃ t, s ⊆ ⋃ (i : ι) (_ : i ∈ t), U i) : IsCompact s

A set s is compact if for every open cover of s, there exists a finite subcover.

theorem isCompact_of_finite_subfamily_closed {α : Type u} [TopologicalSpace α] {s : Set α} (h : ∀ {ι : Type u} (Z : ι → Set α), (∀ (i : ι), IsClosed (Z i)) → s ∩ ⋂ (i : ι), Z i = ∅ → ∃ t, s ∩ ⋂ (i : ι) (_ : i ∈ t), Z i = ∅) : IsCompact s

A set s is compact if for every family of closed sets whose intersection avoids s, there exists a finite subfamily whose intersection avoids s.

theorem isCompact_iff_finite_subcover {α : Type u} [TopologicalSpace α] {s : Set α} : IsCompact s ↔ ∀ {ι : Type u} (U : ι → Set α), (∀ (i : ι), IsOpen (U i)) → s ⊆ ⋃ (i : ι), U i → ∃ t, s ⊆ ⋃ (i : ι) (_ : i ∈ t), U i

A set s is compact if and only if for every open cover of s, there exists a finite subcover.

theorem isCompact_iff_finite_subfamily_closed {α : Type u} [TopologicalSpace α] {s : Set α} : IsCompact s ↔ ∀ {ι : Type u} (Z : ι → Set α), (∀ (i : ι), IsClosed (Z i)) → s ∩ ⋂ (i : ι), Z i = ∅ → ∃ t, s ∩ ⋂ (i : ι) (_ : 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.

theorem IsCompact.mem_nhdsSet_prod_of_forall {α : Type u} {β : Type v} [TopologicalSpace α] {K : Set α} {l : Filter β} {s : Set (α × β)} (hK : IsCompact K) (hs : ∀ (x : α), x ∈ K → s ∈ nhds x ×ˢ l) : s ∈ nhdsSet K ×ˢ l

If s : Set (α × β) belongs to 𝓝 x ×ˢ l for all x from a compact set K, then it belongs to (𝓝ˢ K) ×ˢ l, i.e., there exist an open U ⊇ K and t ∈ l such that U ×ˢ t ⊆ s.

theorem IsCompact.nhdsSet_prod_eq_biSup {α : Type u} {β : Type v} [TopologicalSpace α] {K : Set α} (hK : IsCompact K) (l : Filter β) : nhdsSet K ×ˢ l = ⨆ (x : α) (_ : x ∈ K), nhds x ×ˢ l

theorem IsCompact.prod_nhdsSet_eq_biSup {α : Type u} {β : Type v} [TopologicalSpace β] {K : Set β} (hK : IsCompact K) (l : Filter α) : l ×ˢ nhdsSet K = ⨆ (y : β) (_ : y ∈ K), l ×ˢ nhds y

theorem IsCompact.mem_prod_nhdsSet_of_forall {α : Type u} {β : Type v} [TopologicalSpace β] {K : Set β} {l : Filter α} {s : Set (α × β)} (hK : IsCompact K) (hs : ∀ (y : β), y ∈ K → s ∈ l ×ˢ nhds y) : s ∈ l ×ˢ nhdsSet K

If s : Set (α × β) belongs to l ×ˢ 𝓝 y for all y from a compact set K, then it belongs to l ×ˢ (𝓝ˢ K), i.e., there exist t ∈ l and an open U ⊇ K such that t ×ˢ U ⊆ s.

theorem IsCompact.eventually_forall_of_forall_eventually {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] {x₀ : α} {K : Set β} (hK : IsCompact 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₀).

Provided for backwards compatibility, see IsCompact.mem_prod_nhdsSet_of_forall for a stronger statement.

@[simp]

theorem isCompact_empty {α : Type u} [TopologicalSpace α] : IsCompact ∅

@[simp]

theorem isCompact_singleton {α : Type u} [TopologicalSpace α] {a : α} : IsCompact {a}

theorem Set.Subsingleton.isCompact {α : Type u} [TopologicalSpace α] {s : Set α} (hs : Set.Subsingleton s) : IsCompact s

theorem Set.Finite.isCompact_biUnion {α : Type u} {ι : Type u_1} [TopologicalSpace α] {s : Set ι} {f : ι → Set α} (hs : Set.Finite s) (hf : ∀ (i : ι), i ∈ s → IsCompact (f i)) : IsCompact (⋃ (i : ι) (_ : i ∈ s), f i)

theorem Finset.isCompact_biUnion {α : Type u} {ι : Type u_1} [TopologicalSpace α] (s : Finset ι) {f : ι → Set α} (hf : ∀ (i : ι), i ∈ s → IsCompact (f i)) : IsCompact (⋃ (i : ι) (_ : i ∈ s), f i)

theorem isCompact_accumulate {α : Type u} [TopologicalSpace α] {K : ℕ → Set α} (hK : ∀ (n : ℕ), IsCompact (K n)) (n : ℕ) : IsCompact (Set.Accumulate K n)

theorem Set.Finite.isCompact_sUnion {α : Type u} [TopologicalSpace α] {S : Set (Set α)} (hf : Set.Finite S) (hc : ∀ (s : Set α), s ∈ S → IsCompact s) : IsCompact (⋃₀ S)

theorem isCompact_iUnion {α : Type u} [TopologicalSpace α] {ι : Sort u_3} {f : ι → Set α} [Finite ι] (h : ∀ (i : ι), IsCompact (f i)) : IsCompact (⋃ (i : ι), f i)

theorem Set.Finite.isCompact {α : Type u} [TopologicalSpace α] {s : Set α} (hs : Set.Finite s) : IsCompact s

theorem IsCompact.finite_of_discrete {α : Type u} [TopologicalSpace α] [DiscreteTopology α] {s : Set α} (hs : IsCompact s) : Set.Finite s

theorem isCompact_iff_finite {α : Type u} [TopologicalSpace α] [DiscreteTopology α] {s : Set α} : IsCompact s ↔ Set.Finite s

theorem IsCompact.union {α : Type u} [TopologicalSpace α] {s : Set α} {t : Set α} (hs : IsCompact s) (ht : IsCompact t) : IsCompact (s ∪ t)

theorem IsCompact.insert {α : Type u} [TopologicalSpace α] {s : Set α} (hs : IsCompact s) (a : α) : IsCompact (insert a s)

theorem exists_subset_nhds_of_isCompact' {α : Type u} [TopologicalSpace α] {ι : Type u_3} [Nonempty ι] {V : ι → Set α} (hV : Directed (fun x x_1 => x ⊇ x_1) V) (hV_cpct : ∀ (i : ι), IsCompact (V i)) (hV_closed : ∀ (i : ι), IsClosed (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.

theorem isCompact_open_iff_eq_finite_iUnion_of_isTopologicalBasis {α : Type u} {ι : Type u_1} [TopologicalSpace α] (b : ι → Set α) (hb : TopologicalSpace.IsTopologicalBasis (Set.range b)) (hb' : ∀ (i : ι), IsCompact (b i)) (U : Set α) : IsCompact U ∧ IsOpen U ↔ ∃ s, Set.Finite s ∧ U = ⋃ (i : ι) (_ : 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

def Filter.cocompact (α : Type u_3) [TopologicalSpace α] : Filter α

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

Equations

• Filter.cocompact α = ⨅ (s : Set α) (_ : IsCompact s), Filter.principal sᶜ

theorem Filter.hasBasis_cocompact {α : Type u} [TopologicalSpace α] : Filter.HasBasis (Filter.cocompact α) IsCompact compl

theorem Filter.mem_cocompact {α : Type u} [TopologicalSpace α] {s : Set α} : s ∈ Filter.cocompact α ↔ ∃ t, IsCompact t ∧ tᶜ ⊆ s

theorem Filter.mem_cocompact' {α : Type u} [TopologicalSpace α] {s : Set α} : s ∈ Filter.cocompact α ↔ ∃ t, IsCompact t ∧ sᶜ ⊆ t

theorem IsCompact.compl_mem_cocompact {α : Type u} [TopologicalSpace α] {s : Set α} (hs : IsCompact s) : sᶜ ∈ Filter.cocompact α

theorem Filter.cocompact_le_cofinite {α : Type u} [TopologicalSpace α] : Filter.cocompact α ≤ Filter.cofinite

theorem Filter.cocompact_eq_cofinite (α : Type u_3) [TopologicalSpace α] [DiscreteTopology α] : Filter.cocompact α = Filter.cofinite

@[simp]

theorem Nat.cocompact_eq : Filter.cocompact ℕ = Filter.atTop

theorem Filter.Tendsto.isCompact_insert_range_of_cocompact {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {b : β} (hf : Filter.Tendsto f (Filter.cocompact α) (nhds b)) (hfc : Continuous f) : IsCompact (insert b (Set.range f))

theorem Filter.Tendsto.isCompact_insert_range_of_cofinite {α : Type u} {ι : Type u_1} [TopologicalSpace α] {f : ι → α} {a : α} (hf : Filter.Tendsto f Filter.cofinite (nhds a)) : IsCompact (insert a (Set.range f))

theorem Filter.Tendsto.isCompact_insert_range {α : Type u} [TopologicalSpace α] {f : ℕ → α} {a : α} (hf : Filter.Tendsto f Filter.atTop (nhds a)) : IsCompact (insert a (Set.range f))

def Filter.coclosedCompact (α : Type u_3) [TopologicalSpace α] : Filter α

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

Equations

• Filter.coclosedCompact α = ⨅ (s : Set α) (_ : IsClosed s) (_ : IsCompact s), Filter.principal sᶜ

theorem Filter.hasBasis_coclosedCompact {α : Type u} [TopologicalSpace α] : Filter.HasBasis (Filter.coclosedCompact α) (fun s => IsClosed s ∧ IsCompact s) compl

theorem Filter.mem_coclosedCompact {α : Type u} [TopologicalSpace α] {s : Set α} : s ∈ Filter.coclosedCompact α ↔ ∃ t, IsClosed t ∧ IsCompact t ∧ tᶜ ⊆ s

theorem Filter.mem_coclosed_compact' {α : Type u} [TopologicalSpace α] {s : Set α} : s ∈ Filter.coclosedCompact α ↔ ∃ t, IsClosed t ∧ IsCompact t ∧ sᶜ ⊆ t

theorem Filter.cocompact_le_coclosedCompact {α : Type u} [TopologicalSpace α] : Filter.cocompact α ≤ Filter.coclosedCompact α

theorem IsCompact.compl_mem_coclosedCompact_of_isClosed {α : Type u} [TopologicalSpace α] {s : Set α} (hs : IsCompact s) (hs' : IsClosed s) : sᶜ ∈ Filter.coclosedCompact α

def Bornology.inCompact (α : Type u) [TopologicalSpace α] : Bornology α

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

Equations

• Bornology.inCompact α = { cobounded' := Filter.cocompact α, le_cofinite' := (_ : Filter.cocompact α ≤ Filter.cofinite) }

theorem Bornology.inCompact.isBounded_iff {α : Type u} [TopologicalSpace α] {s : Set α} : Bornology.IsBounded s ↔ ∃ t, IsCompact t ∧ s ⊆ t

theorem IsCompact.nhdsSet_prod_eq {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] {s : Set α} {t : Set β} (hs : IsCompact s) (ht : IsCompact t) : nhdsSet (s ×ˢ t) = nhdsSet s ×ˢ nhdsSet t

If s and t are compact sets, then the set neighborhoods filter of s ×ˢ t is the product of set neighborhoods filters for s and t.

For general sets, only the ≤ inequality holds, see nhdsSet_prod_le.

theorem nhdsSet_prod_le {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] (s : Set α) (t : Set β) : nhdsSet (s ×ˢ t) ≤ nhdsSet s ×ˢ nhdsSet t

The product of a neighborhood of s and a neighborhood of t is a neighborhood of s ×ˢ t, formulated in terms of a filter inequality.

theorem generalized_tube_lemma {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] {s : Set α} (hs : IsCompact s) {t : Set β} (ht : IsCompact t) {n : Set (α × β)} (hn : IsOpen n) (hp : s ×ˢ t ⊆ n) : ∃ u v, IsOpen u ∧ IsOpen 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.

See also IsCompact.nhdsSet_prod_eq.

class CompactSpace (α : Type u_3) [TopologicalSpace α] : Prop

• isCompact_univ : IsCompact Set.univ

  In a compact space, Set.univ is a compact set.

Type class for compact spaces. Separation is sometimes included in the definition, especially in the French literature, but we do not include it here.

instance Subsingleton.compactSpace {α : Type u} [TopologicalSpace α] [Subsingleton α] : CompactSpace α

Equations

• @Subsingleton.compactSpace = @Subsingleton.compactSpace.proof_1

theorem isCompact_univ_iff {α : Type u} [TopologicalSpace α] : IsCompact Set.univ ↔ CompactSpace α

theorem isCompact_univ {α : Type u} [TopologicalSpace α] [h : CompactSpace α] : IsCompact Set.univ

theorem cluster_point_of_compact {α : Type u} [TopologicalSpace α] [CompactSpace α] (f : Filter α) [Filter.NeBot f] : ∃ x, ClusterPt x f

theorem CompactSpace.elim_nhds_subcover {α : Type u} [TopologicalSpace α] [CompactSpace α] (U : α → Set α) (hU : ∀ (x : α), U x ∈ nhds x) : ∃ t, ⋃ (x : α) (_ : x ∈ t), U x = ⊤

theorem compactSpace_of_finite_subfamily_closed {α : Type u} [TopologicalSpace α] (h : ∀ {ι : Type u} (Z : ι → Set α), (∀ (i : ι), IsClosed (Z i)) → ⋂ (i : ι), Z i = ∅ → ∃ t, ⋂ (i : ι) (_ : i ∈ t), Z i = ∅) : CompactSpace α

theorem IsClosed.isCompact {α : Type u} [TopologicalSpace α] [CompactSpace α] {s : Set α} (h : IsClosed s) : IsCompact s

class NoncompactSpace (α : Type u_3) [TopologicalSpace α] : Prop

• noncompact_univ : ¬IsCompact Set.univ

  In a noncompact space, Set.univ is not a compact set.

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

theorem noncompact_univ (α : Type u_3) [TopologicalSpace α] [NoncompactSpace α] : ¬IsCompact Set.univ

theorem IsCompact.ne_univ {α : Type u} [TopologicalSpace α] [NoncompactSpace α] {s : Set α} (hs : IsCompact s) : s ≠ Set.univ

instance instNeBotCocompact {α : Type u} [TopologicalSpace α] [NoncompactSpace α] : Filter.NeBot (Filter.cocompact α)

Equations

• @instNeBotCocompact = @instNeBotCocompact.proof_1

@[simp]

theorem Filter.cocompact_eq_bot {α : Type u} [TopologicalSpace α] [CompactSpace α] : Filter.cocompact α = ⊥

instance instNeBotCoclosedCompact {α : Type u} [TopologicalSpace α] [NoncompactSpace α] : Filter.NeBot (Filter.coclosedCompact α)

Equations

• @instNeBotCoclosedCompact = @instNeBotCoclosedCompact.proof_1

theorem noncompactSpace_of_neBot {α : Type u} [TopologicalSpace α] : Filter.NeBot (Filter.cocompact α) → NoncompactSpace α

theorem Filter.cocompact_neBot_iff {α : Type u} [TopologicalSpace α] : Filter.NeBot (Filter.cocompact α) ↔ NoncompactSpace α

theorem not_compactSpace_iff {α : Type u} [TopologicalSpace α] : ¬CompactSpace α ↔ NoncompactSpace α

instance instNoncompactSpaceIntInstTopologicalSpaceInt : NoncompactSpace ℤ

Equations

• instNoncompactSpaceIntInstTopologicalSpaceInt = instNoncompactSpaceIntInstTopologicalSpaceInt.proof_1

theorem finite_of_compact_of_discrete {α : Type u} [TopologicalSpace α] [CompactSpace α] [DiscreteTopology α] : Finite α

A compact discrete space is finite.

theorem exists_nhds_ne_neBot (α : Type u_3) [TopologicalSpace α] [CompactSpace α] [Infinite α] : ∃ z, Filter.NeBot (nhdsWithin z {z}ᶜ)

theorem finite_cover_nhds_interior {α : Type u} [TopologicalSpace α] [CompactSpace α] {U : α → Set α} (hU : ∀ (x : α), U x ∈ nhds x) : ∃ t, ⋃ (x : α) (_ : x ∈ t), interior (U x) = Set.univ

theorem finite_cover_nhds {α : Type u} [TopologicalSpace α] [CompactSpace α] {U : α → Set α} (hU : ∀ (x : α), U x ∈ nhds x) : ∃ t, ⋃ (x : α) (_ : x ∈ t), U x = Set.univ

theorem LocallyFinite.finite_nonempty_of_compact {α : Type u} [TopologicalSpace α] {ι : Type u_3} [CompactSpace α] {f : ι → Set α} (hf : LocallyFinite f) : Set.Finite {i | Set.Nonempty (f i)}

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

theorem LocallyFinite.finite_of_compact {α : Type u} [TopologicalSpace α] {ι : Type u_3} [CompactSpace α] {f : ι → Set α} (hf : LocallyFinite f) (hne : ∀ (i : ι), Set.Nonempty (f i)) : Set.Finite Set.univ

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

noncomputable def LocallyFinite.fintypeOfCompact {α : Type u} [TopologicalSpace α] {ι : Type u_3} [CompactSpace α] {f : ι → Set α} (hf : LocallyFinite f) (hne : ∀ (i : ι), Set.Nonempty (f i)) : Fintype ι

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

Equations

• LocallyFinite.fintypeOfCompact hf hne = Set.fintypeOfFiniteUniv (_ : Set.Finite Set.univ)

theorem Filter.comap_cocompact_le {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] {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.

theorem isCompact_range {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [CompactSpace α] {f : α → β} (hf : Continuous f) : IsCompact (Set.range f)

theorem isCompact_diagonal {α : Type u} [TopologicalSpace α] [CompactSpace α] : IsCompact (Set.diagonal α)

theorem isClosedMap_snd_of_compactSpace {X : Type u_3} [TopologicalSpace X] [CompactSpace X] {Y : Type u_4} [TopologicalSpace Y] : IsClosedMap Prod.snd

If X is a compact topological space, then Prod.snd : X × Y → Y is a closed map.

theorem exists_subset_nhds_of_compactSpace {α : Type u} [TopologicalSpace α] [CompactSpace α] {ι : Type u_3} [Nonempty ι] {V : ι → Set α} (hV : Directed (fun x x_1 => x ⊇ x_1) V) (hV_closed : ∀ (i : ι), IsClosed (V i)) {U : Set α} (hU : ∀ (x : α), x ∈ ⋂ (i : ι), V i → U ∈ nhds x) : ∃ i, V i ⊆ U

theorem Inducing.isCompact_iff {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} (hf : Inducing f) {s : Set α} : IsCompact (f '' s) ↔ IsCompact s

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

theorem Embedding.isCompact_iff_isCompact_image {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] {s : Set α} {f : α → β} (hf : Embedding f) : IsCompact s ↔ IsCompact (f '' s)

If f : α → β is an Embedding (or more generally, an Inducing map, see Inducing.isCompact_iff), the image f '' s of a set s is compact if and only if the set s is compact.

theorem Inducing.isCompact_preimage {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} (hf : Inducing f) (hf' : IsClosed (Set.range f)) {K : Set β} (hK : IsCompact K) : IsCompact (f ⁻¹' K)

The preimage of a compact set under an inducing map is a compact set.

theorem ClosedEmbedding.isCompact_preimage {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} (hf : ClosedEmbedding f) {K : Set β} (hK : IsCompact K) : IsCompact (f ⁻¹' K)

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

theorem ClosedEmbedding.tendsto_cocompact {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} (hf : ClosedEmbedding 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 ClosedEmbedding.isCompact_preimage.

theorem isCompact_iff_isCompact_in_subtype {α : Type u} [TopologicalSpace α] {p : α → Prop} {s : Set { a // p a }} : IsCompact s ↔ IsCompact (Subtype.val '' s)

theorem isCompact_iff_isCompact_univ {α : Type u} [TopologicalSpace α] {s : Set α} : IsCompact s ↔ IsCompact Set.univ

theorem isCompact_iff_compactSpace {α : Type u} [TopologicalSpace α] {s : Set α} : IsCompact s ↔ CompactSpace ↑s

theorem IsCompact.finite {α : Type u} [TopologicalSpace α] {s : Set α} (hs : IsCompact s) (hs' : DiscreteTopology ↑s) : Set.Finite s

theorem exists_nhds_ne_inf_principal_neBot {α : Type u} [TopologicalSpace α] {s : Set α} (hs : IsCompact s) (hs' : Set.Infinite s) : ∃ z, z ∈ s ∧ Filter.NeBot (nhdsWithin z {z}ᶜ ⊓ Filter.principal s)

theorem ClosedEmbedding.noncompactSpace {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [NoncompactSpace α] {f : α → β} (hf : ClosedEmbedding f) : NoncompactSpace β

theorem ClosedEmbedding.compactSpace {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [h : CompactSpace β] {f : α → β} (hf : ClosedEmbedding f) : CompactSpace α

theorem IsCompact.prod {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] {s : Set α} {t : Set β} (hs : IsCompact s) (ht : IsCompact t) : IsCompact (s ×ˢ t)

instance Finite.compactSpace {α : Type u} [TopologicalSpace α] [Finite α] : CompactSpace α

Finite topological spaces are compact.

Equations

• @Finite.compactSpace = @Finite.compactSpace.proof_1

instance instCompactSpaceProdInstTopologicalSpaceProd {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [CompactSpace α] [CompactSpace β] : CompactSpace (α × β)

The product of two compact spaces is compact.

Equations

• @instCompactSpaceProdInstTopologicalSpaceProd = @instCompactSpaceProdInstTopologicalSpaceProd.proof_1

instance instCompactSpaceSumInstTopologicalSpaceSum {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [CompactSpace α] [CompactSpace β] : CompactSpace (α ⊕ β)

The disjoint union of two compact spaces is compact.

Equations

• @instCompactSpaceSumInstTopologicalSpaceSum = @instCompactSpaceSumInstTopologicalSpaceSum.proof_1

instance instCompactSpaceSigmaInstTopologicalSpaceSigma {ι : Type u_1} {π : ι → Type u_2} [Finite ι] [(i : ι) → TopologicalSpace (π i)] [∀ (i : ι), CompactSpace (π i)] : CompactSpace ((i : ι) × π i)

Equations

• @instCompactSpaceSigmaInstTopologicalSpaceSigma = @instCompactSpaceSigmaInstTopologicalSpaceSigma.proof_1

theorem Filter.coprod_cocompact {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] : Filter.coprod (Filter.cocompact α) (Filter.cocompact β) = Filter.cocompact (α × β)

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

theorem Prod.noncompactSpace_iff {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] : NoncompactSpace (α × β) ↔ NoncompactSpace α ∧ Nonempty β ∨ Nonempty α ∧ NoncompactSpace β

instance Prod.noncompactSpace_left {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [NoncompactSpace α] [Nonempty β] : NoncompactSpace (α × β)

Equations

• @Prod.noncompactSpace_left = @Prod.noncompactSpace_left.proof_1

instance Prod.noncompactSpace_right {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [Nonempty α] [NoncompactSpace β] : NoncompactSpace (α × β)

Equations

• @Prod.noncompactSpace_right = @Prod.noncompactSpace_right.proof_1

theorem isCompact_pi_infinite {ι : Type u_1} {π : ι → Type u_2} [(i : ι) → TopologicalSpace (π i)] {s : (i : ι) → Set (π i)} : (∀ (i : ι), IsCompact (s i)) → IsCompact {x | ∀ (i : ι), x i ∈ s i}

Tychonoff's theorem: product of compact sets is compact.

theorem isCompact_univ_pi {ι : Type u_1} {π : ι → Type u_2} [(i : ι) → TopologicalSpace (π i)] {s : (i : ι) → Set (π i)} (h : ∀ (i : ι), IsCompact (s i)) : IsCompact (Set.pi Set.univ s)

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

instance Pi.compactSpace {ι : Type u_1} {π : ι → Type u_2} [(i : ι) → TopologicalSpace (π i)] [∀ (i : ι), CompactSpace (π i)] : CompactSpace ((i : ι) → π i)

Equations

• @Pi.compactSpace = @Pi.compactSpace.proof_1

instance Function.compactSpace {β : Type v} {ι : Type u_1} [TopologicalSpace β] [CompactSpace β] : CompactSpace (ι → β)

Equations

• @Function.compactSpace = @Function.compactSpace.proof_1

theorem Filter.coprodᵢ_cocompact {δ : Type u_3} {κ : δ → Type u_4} [(d : δ) → TopologicalSpace (κ d)] : (Filter.coprodᵢ fun 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.

instance Quot.compactSpace {α : Type u} [TopologicalSpace α] {r : α → α → Prop} [CompactSpace α] : CompactSpace (Quot r)

Equations

• @Quot.compactSpace = @Quot.compactSpace.proof_1

instance Quotient.compactSpace {α : Type u} [TopologicalSpace α] {s : Setoid α} [CompactSpace α] : CompactSpace (Quotient s)

Equations

• @Quotient.compactSpace = @Quotient.compactSpace.proof_1

class WeaklyLocallyCompactSpace (α : Type u_3) [TopologicalSpace α] : Prop

• exists_compact_mem_nhds : ∀ (x : α), ∃ s, IsCompact s ∧ s ∈ nhds x

  Every point of a weakly locally compact space admits a compact neighborhood.

We say that a topological space is a weakly locally compact space, if each point of this space admits a compact neighborhood.

instance instWeaklyLocallyCompactSpaceProdInstTopologicalSpaceProd {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [WeaklyLocallyCompactSpace α] [WeaklyLocallyCompactSpace β] : WeaklyLocallyCompactSpace (α × β)

Equations

• @instWeaklyLocallyCompactSpaceProdInstTopologicalSpaceProd = @instWeaklyLocallyCompactSpaceProdInstTopologicalSpaceProd.proof_1

instance instWeaklyLocallyCompactSpaceForAllTopologicalSpace {ι : Type u_3} [Finite ι] {X : ι → Type u_4} [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), WeaklyLocallyCompactSpace (X i)] : WeaklyLocallyCompactSpace ((i : ι) → X i)

Equations

• @instWeaklyLocallyCompactSpaceForAllTopologicalSpace = @instWeaklyLocallyCompactSpaceForAllTopologicalSpace.proof_1

instance instWeaklyLocallyCompactSpace {α : Type u} [TopologicalSpace α] [CompactSpace α] : WeaklyLocallyCompactSpace α

Equations

• @instWeaklyLocallyCompactSpace = @instWeaklyLocallyCompactSpace.proof_1

theorem exists_compact_superset {α : Type u} [TopologicalSpace α] [WeaklyLocallyCompactSpace α] {K : Set α} (hK : IsCompact K) : ∃ K', IsCompact K' ∧ K ⊆ interior K'

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

theorem disjoint_nhds_cocompact {α : Type u} [TopologicalSpace α] [WeaklyLocallyCompactSpace α] (x : α) : Disjoint (nhds x) (Filter.cocompact α)

In a weakly locally compact space, the filters 𝓝 x and cocompact α are disjoint for all α.

class LocallyCompactSpace (α : Type u_3) [TopologicalSpace α] : Prop

• local_compact_nhds : ∀ (x : α) (n : Set α), n ∈ nhds x → ∃ s, s ∈ nhds x ∧ s ⊆ n ∧ IsCompact s

  In a locally compact space, every neighbourhood of every point contains a compact neighbourhood of that same point.

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.

See also WeaklyLocallyCompactSpace, a typeclass that only assumes that each point has a compact neighborhood.

theorem compact_basis_nhds {α : Type u} [TopologicalSpace α] [LocallyCompactSpace α] (x : α) : Filter.HasBasis (nhds x) (fun s => s ∈ nhds x ∧ IsCompact s) fun s => s

theorem local_compact_nhds {α : Type u} [TopologicalSpace α] [LocallyCompactSpace α] {x : α} {n : Set α} (h : n ∈ nhds x) : ∃ s, s ∈ nhds x ∧ s ⊆ n ∧ IsCompact s

theorem locallyCompactSpace_of_hasBasis {α : Type u} [TopologicalSpace α] {ι : α → Type u_3} {p : (x : α) → ι x → Prop} {s : (x : α) → ι x → Set α} (h : ∀ (x : α), Filter.HasBasis (nhds x) (p x) (s x)) (hc : ∀ (x : α) (i : ι x), p x i → IsCompact (s x i)) : LocallyCompactSpace α

instance Prod.locallyCompactSpace (α : Type u_3) (β : Type u_4) [TopologicalSpace α] [TopologicalSpace β] [LocallyCompactSpace α] [LocallyCompactSpace β] : LocallyCompactSpace (α × β)

Equations

• Prod.locallyCompactSpace = Prod.locallyCompactSpace.proof_1

instance Pi.locallyCompactSpace_of_finite {ι : Type u_1} {π : ι → Type u_2} [(i : ι) → TopologicalSpace (π i)] [∀ (i : ι), LocallyCompactSpace (π i)] [Finite ι] : LocallyCompactSpace ((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.

Equations

• @Pi.locallyCompactSpace_of_finite = @Pi.locallyCompactSpace_of_finite.proof_1

instance Pi.locallyCompactSpace {ι : Type u_1} {π : ι → Type u_2} [(i : ι) → TopologicalSpace (π i)] [∀ (i : ι), LocallyCompactSpace (π i)] [∀ (i : ι), CompactSpace (π i)] : LocallyCompactSpace ((i : ι) → π i)

For spaces that are not Hausdorff.

Equations

• @Pi.locallyCompactSpace = @Pi.locallyCompactSpace.proof_1

instance Function.locallyCompactSpace_of_finite {β : Type v} {ι : Type u_1} [TopologicalSpace β] [Finite ι] [LocallyCompactSpace β] : LocallyCompactSpace (ι → β)

Equations

• @Function.locallyCompactSpace_of_finite = @Function.locallyCompactSpace_of_finite.proof_1

instance Function.locallyCompactSpace {β : Type v} {ι : Type u_1} [TopologicalSpace β] [LocallyCompactSpace β] [CompactSpace β] : LocallyCompactSpace (ι → β)

Equations

• @Function.locallyCompactSpace = @Function.locallyCompactSpace.proof_1

theorem exists_compact_subset {α : Type u} [TopologicalSpace α] [LocallyCompactSpace α] {x : α} {U : Set α} (hU : IsOpen U) (hx : x ∈ U) : ∃ K, IsCompact 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.

instance instWeaklyLocallyCompactSpace_1 {α : Type u} [TopologicalSpace α] [LocallyCompactSpace α] : WeaklyLocallyCompactSpace α

Equations

• @instWeaklyLocallyCompactSpace_1 = @instWeaklyLocallyCompactSpace_1.proof_1

theorem exists_compact_between {α : Type u} [TopologicalSpace α] [hα : LocallyCompactSpace α] {K : Set α} {U : Set α} (hK : IsCompact K) (hU : IsOpen U) (h_KU : K ⊆ U) : ∃ L, IsCompact L ∧ K ⊆ interior L ∧ L ⊆ U

In a locally compact space, for every containment 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.

theorem ClosedEmbedding.locallyCompactSpace {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [LocallyCompactSpace β] {f : α → β} (hf : ClosedEmbedding f) : LocallyCompactSpace α

theorem IsClosed.locallyCompactSpace {α : Type u} [TopologicalSpace α] [LocallyCompactSpace α] {s : Set α} (hs : IsClosed s) : LocallyCompactSpace ↑s

theorem OpenEmbedding.locallyCompactSpace {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [LocallyCompactSpace β] {f : α → β} (hf : OpenEmbedding f) : LocallyCompactSpace α

theorem IsOpen.locallyCompactSpace {α : Type u} [TopologicalSpace α] [LocallyCompactSpace α] {s : Set α} (hs : IsOpen s) : LocallyCompactSpace ↑s

theorem Ultrafilter.le_nhds_lim {α : Type u} [TopologicalSpace α] [CompactSpace α] (F : Ultrafilter α) : ↑F ≤ nhds (Ultrafilter.lim F)

theorem IsClosed.exists_minimal_nonempty_closed_subset {α : Type u} [TopologicalSpace α] [CompactSpace α] {S : Set α} (hS : IsClosed S) (hne : Set.Nonempty S) : ∃ V, V ⊆ S ∧ Set.Nonempty V ∧ IsClosed V ∧ ∀ (V' : Set α), V' ⊆ V → Set.Nonempty V' → IsClosed V' → V' = V

class SigmaCompactSpace (α : Type u_3) [TopologicalSpace α] : Prop

• exists_compact_covering : ∃ K, (∀ (n : ℕ), IsCompact (K n)) ∧ ⋃ (n : ℕ), K n = Set.univ

  In a σ-compact space, there exists (by definition) a countable collection of compact subspaces that cover the entire space.

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

instance CompactSpace.sigma_compact {α : Type u} [TopologicalSpace α] [CompactSpace α] : SigmaCompactSpace α

Equations

• @CompactSpace.sigma_compact = @CompactSpace.sigma_compact.proof_1

theorem SigmaCompactSpace.of_countable {α : Type u} [TopologicalSpace α] (S : Set (Set α)) (Hc : Set.Countable S) (Hcomp : ∀ (s : Set α), s ∈ S → IsCompact s) (HU : ⋃₀ S = Set.univ) : SigmaCompactSpace α

instance sigmaCompactSpace_of_locally_compact_second_countable {α : Type u} [TopologicalSpace α] [LocallyCompactSpace α] [TopologicalSpace.SecondCountableTopology α] : SigmaCompactSpace α

Equations

• @sigmaCompactSpace_of_locally_compact_second_countable = @sigmaCompactSpace_of_locally_compact_second_countable.proof_1

def compactCovering (α : Type u) [TopologicalSpace α] [SigmaCompactSpace α] : ℕ → Set α

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

Equations

• compactCovering α = Set.Accumulate (Exists.choose (_ : ∃ K, (∀ (n : ℕ), IsCompact (K n)) ∧ ⋃ (n : ℕ), K n = Set.univ))

theorem isCompact_compactCovering (α : Type u) [TopologicalSpace α] [SigmaCompactSpace α] (n : ℕ) : IsCompact (compactCovering α n)

theorem iUnion_compactCovering (α : Type u) [TopologicalSpace α] [SigmaCompactSpace α] : ⋃ (n : ℕ), compactCovering α n = Set.univ

theorem compactCovering_subset (α : Type u) [TopologicalSpace α] [SigmaCompactSpace α] ⦃m : ℕ⦄ ⦃n : ℕ⦄ (h : m ≤ n) : compactCovering α m ⊆ compactCovering α n

theorem exists_mem_compactCovering {α : Type u} [TopologicalSpace α] [SigmaCompactSpace α] (x : α) : ∃ n, x ∈ compactCovering α n

instance instSigmaCompactSpaceProdInstTopologicalSpaceProd {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [SigmaCompactSpace α] [SigmaCompactSpace β] : SigmaCompactSpace (α × β)

Equations

• @instSigmaCompactSpaceProdInstTopologicalSpaceProd = @instSigmaCompactSpaceProdInstTopologicalSpaceProd.proof_1

instance instSigmaCompactSpaceForAllTopologicalSpace {ι : Type u_1} {π : ι → Type u_2} [Finite ι] [(i : ι) → TopologicalSpace (π i)] [∀ (i : ι), SigmaCompactSpace (π i)] : SigmaCompactSpace ((i : ι) → π i)

Equations

• @instSigmaCompactSpaceForAllTopologicalSpace = @instSigmaCompactSpaceForAllTopologicalSpace.proof_1

instance instSigmaCompactSpaceSumInstTopologicalSpaceSum {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [SigmaCompactSpace α] [SigmaCompactSpace β] : SigmaCompactSpace (α ⊕ β)

Equations

• @instSigmaCompactSpaceSumInstTopologicalSpaceSum = @instSigmaCompactSpaceSumInstTopologicalSpaceSum.proof_1

instance instSigmaCompactSpaceSigmaInstTopologicalSpaceSigma {ι : Type u_1} {π : ι → Type u_2} [Countable ι] [(i : ι) → TopologicalSpace (π i)] [∀ (i : ι), SigmaCompactSpace (π i)] : SigmaCompactSpace ((i : ι) × π i)

Equations

• @instSigmaCompactSpaceSigmaInstTopologicalSpaceSigma = @instSigmaCompactSpaceSigmaInstTopologicalSpaceSigma.proof_1

theorem ClosedEmbedding.sigmaCompactSpace {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [SigmaCompactSpace α] {e : β → α} (he : ClosedEmbedding e) : SigmaCompactSpace β

theorem IsClosed.sigmaCompactSpace {α : Type u} [TopologicalSpace α] [SigmaCompactSpace α] {s : Set α} (hs : IsClosed s) : SigmaCompactSpace ↑s

instance instSigmaCompactSpaceULiftTopologicalSpace {β : Type v} [TopologicalSpace β] [SigmaCompactSpace β] : SigmaCompactSpace (ULift.{u, v} β)

Equations

• @instSigmaCompactSpaceULiftTopologicalSpace = @instSigmaCompactSpaceULiftTopologicalSpace.proof_1

theorem LocallyFinite.countable_univ {α : Type u} [TopologicalSpace α] [SigmaCompactSpace α] {ι : Type u_3} {f : ι → Set α} (hf : LocallyFinite f) (hne : ∀ (i : ι), Set.Nonempty (f i)) : Set.Countable Set.univ

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

noncomputable def LocallyFinite.encodable {α : Type u} [TopologicalSpace α] [SigmaCompactSpace α] {ι : Type u_3} {f : ι → Set α} (hf : LocallyFinite f) (hne : ∀ (i : ι), Set.Nonempty (f i)) : Encodable ι

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

Equations

• LocallyFinite.encodable hf hne = Encodable.ofEquiv (↑Set.univ) (Equiv.Set.univ ι).symm

theorem countable_cover_nhdsWithin_of_sigma_compact {α : Type u} [TopologicalSpace α] [SigmaCompactSpace α] {f : α → Set α} {s : Set α} (hs : IsClosed s) (hf : ∀ (x : α), x ∈ s → f x ∈ nhdsWithin x s) : ∃ t x, Set.Countable t ∧ s ⊆ ⋃ (x : α) (_ : 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.

theorem countable_cover_nhds_of_sigma_compact {α : Type u} [TopologicalSpace α] [SigmaCompactSpace α] {f : α → Set α} (hf : ∀ (x : α), f x ∈ nhds x) : ∃ s, Set.Countable s ∧ ⋃ (x : α) (_ : 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.

structure CompactExhaustion (X : Type u_3) [TopologicalSpace X] : Type u_3

• toFun : ℕ → Set X

  The sequence of compact sets that form a compact exhaustion.

• isCompact' : ∀ (n : ℕ), IsCompact (CompactExhaustion.toFun s n)

  The sets in the compact exhaustion are in fact compact.

• subset_interior_succ' : ∀ (n : ℕ), CompactExhaustion.toFun s n ⊆ interior (CompactExhaustion.toFun s (n + 1))

  The sets in the compact exhaustion form a sequence: each set is contained in the interior of the next.

• iUnion_eq' : ⋃ (n : ℕ), CompactExhaustion.toFun s n = Set.univ

  The union of all sets in a compact exhaustion equals the entire space.

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 CompactExhaustion.choice X provides a choice of an exhaustion by compact sets. This choice is also available as (default : CompactExhaustion X).

instance CompactExhaustion.instRelHomClassCompactExhaustionNatSetLeInstLENatSubsetInstHasSubsetSet {α : Type u} [TopologicalSpace α] : RelHomClass (CompactExhaustion α) LE.le Subset

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CompactExhaustion.toFun_eq_coe {α : Type u} [TopologicalSpace α] (K : CompactExhaustion α) : K.toFun = ↑K

theorem CompactExhaustion.isCompact {α : Type u} [TopologicalSpace α] (K : CompactExhaustion α) (n : ℕ) : IsCompact (↑K n)

theorem CompactExhaustion.subset_interior_succ {α : Type u} [TopologicalSpace α] (K : CompactExhaustion α) (n : ℕ) : ↑K n ⊆ interior (↑K (n + 1))

theorem CompactExhaustion.subset {α : Type u} [TopologicalSpace α] (K : CompactExhaustion α) ⦃m : ℕ⦄ ⦃n : ℕ⦄ (h : m ≤ n) : ↑K m ⊆ ↑K n

theorem CompactExhaustion.subset_succ {α : Type u} [TopologicalSpace α] (K : CompactExhaustion α) (n : ℕ) : ↑K n ⊆ ↑K (n + 1)

theorem CompactExhaustion.subset_interior {α : Type u} [TopologicalSpace α] (K : CompactExhaustion α) ⦃m : ℕ⦄ ⦃n : ℕ⦄ (h : m < n) : ↑K m ⊆ interior (↑K n)

theorem CompactExhaustion.iUnion_eq {α : Type u} [TopologicalSpace α] (K : CompactExhaustion α) : ⋃ (n : ℕ), ↑K n = Set.univ

theorem CompactExhaustion.exists_mem {α : Type u} [TopologicalSpace α] (K : CompactExhaustion α) (x : α) : ∃ n, x ∈ ↑K n

noncomputable def CompactExhaustion.find {α : Type u} [TopologicalSpace α] (K : CompactExhaustion α) (x : α) : ℕ

The minimal n such that x ∈ K n.

Equations

• CompactExhaustion.find K x = Nat.find (_ : ∃ n, x ∈ ↑K n)

theorem CompactExhaustion.mem_find {α : Type u} [TopologicalSpace α] (K : CompactExhaustion α) (x : α) : x ∈ ↑K (CompactExhaustion.find K x)

theorem CompactExhaustion.mem_iff_find_le {α : Type u} [TopologicalSpace α] (K : CompactExhaustion α) {x : α} {n : ℕ} : x ∈ ↑K n ↔ CompactExhaustion.find K x ≤ n

def CompactExhaustion.shiftr {α : Type u} [TopologicalSpace α] (K : CompactExhaustion α) : CompactExhaustion α

Prepend the empty set to a compact exhaustion K n.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CompactExhaustion.find_shiftr {α : Type u} [TopologicalSpace α] (K : CompactExhaustion α) (x : α) : CompactExhaustion.find (CompactExhaustion.shiftr K) x = CompactExhaustion.find K x + 1

theorem CompactExhaustion.mem_diff_shiftr_find {α : Type u} [TopologicalSpace α] (K : CompactExhaustion α) (x : α) : x ∈ ↑(CompactExhaustion.shiftr K) (CompactExhaustion.find K x + 1) \ ↑(CompactExhaustion.shiftr K) (CompactExhaustion.find K x)

noncomputable def CompactExhaustion.choice (X : Type u_3) [TopologicalSpace X] [WeaklyLocallyCompactSpace X] [SigmaCompactSpace X] : CompactExhaustion X

A choice of an exhaustion by compact sets of a weakly locally compact σ-compact space.

Equations

• CompactExhaustion.choice X = Classical.choice (_ : Nonempty (CompactExhaustion X))

noncomputable instance CompactExhaustion.instInhabitedCompactExhaustion {α : Type u} [TopologicalSpace α] [LocallyCompactSpace α] [SigmaCompactSpace α] : Inhabited (CompactExhaustion α)

Equations

• CompactExhaustion.instInhabitedCompactExhaustion = { default := CompactExhaustion.choice α }

def IsClopen {α : Type u} [TopologicalSpace α] (s : Set α) : Prop

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

Equations

• IsClopen s = (IsOpen s ∧ IsClosed s)

theorem IsClopen.isOpen {α : Type u} [TopologicalSpace α] {s : Set α} (hs : IsClopen s) : IsOpen s

theorem IsClopen.isClosed {α : Type u} [TopologicalSpace α] {s : Set α} (hs : IsClopen s) : IsClosed s

theorem isClopen_iff_frontier_eq_empty {α : Type u} [TopologicalSpace α] {s : Set α} : IsClopen s ↔ frontier s = ∅

theorem IsClopen.frontier_eq {α : Type u} [TopologicalSpace α] {s : Set α} : IsClopen s → frontier s = ∅

Alias of the forward direction of isClopen_iff_frontier_eq_empty.

theorem IsClopen.union {α : Type u} [TopologicalSpace α] {s : Set α} {t : Set α} (hs : IsClopen s) (ht : IsClopen t) : IsClopen (s ∪ t)

theorem IsClopen.inter {α : Type u} [TopologicalSpace α] {s : Set α} {t : Set α} (hs : IsClopen s) (ht : IsClopen t) : IsClopen (s ∩ t)

@[simp]

theorem isClopen_empty {α : Type u} [TopologicalSpace α] : IsClopen ∅

@[simp]

theorem isClopen_univ {α : Type u} [TopologicalSpace α] : IsClopen Set.univ

theorem IsClopen.compl {α : Type u} [TopologicalSpace α] {s : Set α} (hs : IsClopen s) : IsClopen sᶜ

@[simp]

theorem isClopen_compl_iff {α : Type u} [TopologicalSpace α] {s : Set α} : IsClopen sᶜ ↔ IsClopen s

theorem IsClopen.diff {α : Type u} [TopologicalSpace α] {s : Set α} {t : Set α} (hs : IsClopen s) (ht : IsClopen t) : IsClopen (s \ t)

theorem IsClopen.prod {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] {s : Set α} {t : Set β} (hs : IsClopen s) (ht : IsClopen t) : IsClopen (s ×ˢ t)

theorem isClopen_iUnion_of_finite {α : Type u} [TopologicalSpace α] {β : Type u_3} [Finite β] {s : β → Set α} (h : ∀ (i : β), IsClopen (s i)) : IsClopen (⋃ (i : β), s i)

theorem Set.Finite.isClopen_biUnion {α : Type u} [TopologicalSpace α] {β : Type u_3} {s : Set β} {f : β → Set α} (hs : Set.Finite s) (h : ∀ (i : β), i ∈ s → IsClopen (f i)) : IsClopen (⋃ (i : β) (_ : i ∈ s), f i)

theorem isClopen_biUnion_finset {α : Type u} [TopologicalSpace α] {β : Type u_3} {s : Finset β} {f : β → Set α} (h : ∀ (i : β), i ∈ s → IsClopen (f i)) : IsClopen (⋃ (i : β) (_ : i ∈ s), f i)

theorem isClopen_iInter_of_finite {α : Type u} [TopologicalSpace α] {β : Type u_3} [Finite β] {s : β → Set α} (h : ∀ (i : β), IsClopen (s i)) : IsClopen (⋂ (i : β), s i)

theorem Set.Finite.isClopen_biInter {α : Type u} [TopologicalSpace α] {β : Type u_3} {s : Set β} (hs : Set.Finite s) {f : β → Set α} (h : ∀ (i : β), i ∈ s → IsClopen (f i)) : IsClopen (⋂ (i : β) (_ : i ∈ s), f i)

theorem isClopen_biInter_finset {α : Type u} [TopologicalSpace α] {β : Type u_3} {s : Finset β} {f : β → Set α} (h : ∀ (i : β), i ∈ s → IsClopen (f i)) : IsClopen (⋂ (i : β) (_ : i ∈ s), f i)

theorem IsClopen.preimage {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] {s : Set β} (h : IsClopen s) {f : α → β} (hf : Continuous f) : IsClopen (f ⁻¹' s)

theorem ContinuousOn.preimage_clopen_of_clopen {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s : Set α} {t : Set β} (hf : ContinuousOn f s) (hs : IsClopen s) (ht : IsClopen t) : IsClopen (s ∩ f ⁻¹' t)

theorem isClopen_inter_of_disjoint_cover_clopen {α : Type u} [TopologicalSpace α] {Z : Set α} {a : Set α} {b : Set α} (h : IsClopen Z) (cover : Z ⊆ a ∪ b) (ha : IsOpen a) (hb : IsOpen b) (hab : Disjoint a b) : IsClopen (Z ∩ a)

The intersection of a disjoint covering by two open sets of a clopen set will be clopen.

@[simp]

theorem isClopen_discrete {α : Type u} [TopologicalSpace α] [DiscreteTopology α] (x : Set α) : IsClopen x

theorem isClopen_range_inl {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] : IsClopen (Set.range Sum.inl)

theorem isClopen_range_inr {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] : IsClopen (Set.range Sum.inr)

theorem isClopen_range_sigmaMk {ι : Type u_3} {σ : ι → Type u_4} [(i : ι) → TopologicalSpace (σ i)] {i : ι} : IsClopen (Set.range (Sigma.mk i))

theorem QuotientMap.isClopen_preimage {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} (hf : QuotientMap f) {s : Set β} : IsClopen (f ⁻¹' s) ↔ IsClopen s

theorem continuous_boolIndicator_iff_clopen {X : Type u_3} [TopologicalSpace X] (U : Set X) : Continuous (Set.boolIndicator U) ↔ IsClopen U

theorem continuousOn_boolIndicator_iff_clopen {X : Type u_3} [TopologicalSpace X] (s : Set X) (U : Set X) : ContinuousOn (Set.boolIndicator U) s ↔ IsClopen (Subtype.val ⁻¹' U)

def IsPreirreducible {α : Type u} [TopologicalSpace α] (s : Set α) : Prop

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

Equations

• IsPreirreducible s = ∀ (u v : Set α), IsOpen u → IsOpen v → Set.Nonempty (s ∩ u) → Set.Nonempty (s ∩ v) → Set.Nonempty (s ∩ (u ∩ v))

def IsIrreducible {α : Type u} [TopologicalSpace α] (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

• IsIrreducible s = (Set.Nonempty s ∧ IsPreirreducible s)

theorem IsIrreducible.nonempty {α : Type u} [TopologicalSpace α] {s : Set α} (h : IsIrreducible s) : Set.Nonempty s

theorem IsIrreducible.isPreirreducible {α : Type u} [TopologicalSpace α] {s : Set α} (h : IsIrreducible s) : IsPreirreducible s

theorem isPreirreducible_empty {α : Type u} [TopologicalSpace α] : IsPreirreducible ∅

theorem Set.Subsingleton.isPreirreducible {α : Type u} [TopologicalSpace α] {s : Set α} (hs : Set.Subsingleton s) : IsPreirreducible s

theorem isPreirreducible_singleton {α : Type u} [TopologicalSpace α] {x : α} : IsPreirreducible {x}

theorem isIrreducible_singleton {α : Type u} [TopologicalSpace α] {x : α} : IsIrreducible {x}

theorem isPreirreducible_iff_closure {α : Type u} [TopologicalSpace α] {s : Set α} : IsPreirreducible (closure s) ↔ IsPreirreducible s

theorem isIrreducible_iff_closure {α : Type u} [TopologicalSpace α] {s : Set α} : IsIrreducible (closure s) ↔ IsIrreducible s

theorem IsPreirreducible.closure {α : Type u} [TopologicalSpace α] {s : Set α} : IsPreirreducible s → IsPreirreducible (closure s)

Alias of the reverse direction of isPreirreducible_iff_closure.

theorem IsIrreducible.closure {α : Type u} [TopologicalSpace α] {s : Set α} : IsIrreducible s → IsIrreducible (closure s)

Alias of the reverse direction of isIrreducible_iff_closure.

theorem exists_preirreducible {α : Type u} [TopologicalSpace α] (s : Set α) (H : IsPreirreducible s) : ∃ t, IsPreirreducible t ∧ s ⊆ t ∧ ∀ (u : Set α), IsPreirreducible u → t ⊆ u → u = t

def irreducibleComponents (α : Type u_3) [TopologicalSpace α] : Set (Set α)

The set of irreducible components of a topological space.

Equations

• irreducibleComponents α = maximals (fun x x_1 => x ≤ x_1) {s | IsIrreducible s}

theorem isClosed_of_mem_irreducibleComponents {α : Type u} [TopologicalSpace α] (s : Set α) (H : s ∈ irreducibleComponents α) : IsClosed s

theorem irreducibleComponents_eq_maximals_closed (α : Type u_3) [TopologicalSpace α] : irreducibleComponents α = maximals (fun x x_1 => x ≤ x_1) {s | IsClosed s ∧ IsIrreducible s}

def irreducibleComponent {α : Type u} [TopologicalSpace α] (x : α) : Set α

A maximal irreducible set that contains a given point.

Equations

• irreducibleComponent x = Classical.choose (_ : ∃ t, IsPreirreducible t ∧ {x} ⊆ t ∧ ∀ (u : Set α), IsPreirreducible u → t ⊆ u → u = t)

theorem irreducibleComponent_property {α : Type u} [TopologicalSpace α] (x : α) : IsPreirreducible (irreducibleComponent x) ∧ {x} ⊆ irreducibleComponent x ∧ ∀ (u : Set α), IsPreirreducible u → irreducibleComponent x ⊆ u → u = irreducibleComponent x

theorem mem_irreducibleComponent {α : Type u} [TopologicalSpace α] {x : α} : x ∈ irreducibleComponent x

theorem isIrreducible_irreducibleComponent {α : Type u} [TopologicalSpace α] {x : α} : IsIrreducible (irreducibleComponent x)

theorem eq_irreducibleComponent {α : Type u} [TopologicalSpace α] {x : α} {s : Set α} : IsPreirreducible s → irreducibleComponent x ⊆ s → s = irreducibleComponent x

theorem irreducibleComponent_mem_irreducibleComponents {α : Type u} [TopologicalSpace α] (x : α) : irreducibleComponent x ∈ irreducibleComponents α

theorem isClosed_irreducibleComponent {α : Type u} [TopologicalSpace α] {x : α} : IsClosed (irreducibleComponent x)

class PreirreducibleSpace (α : Type u) [TopologicalSpace α] : Prop

• isPreirreducible_univ : IsPreirreducible Set.univ

  In a preirreducible space, Set.univ is a preirreducible set.

A preirreducible space is one where there is no non-trivial pair of disjoint opens.

class IrreducibleSpace (α : Type u) [TopologicalSpace α] extends PreirreducibleSpace : Prop

• isPreirreducible_univ : IsPreirreducible Set.univ
• toNonempty : Nonempty α

An irreducible space is one that is nonempty and where there is no non-trivial pair of disjoint opens.

theorem IrreducibleSpace.isIrreducible_univ (α : Type u) [TopologicalSpace α] [IrreducibleSpace α] : IsIrreducible Set.univ

theorem irreducibleSpace_def (α : Type u) [TopologicalSpace α] : IrreducibleSpace α ↔ IsIrreducible ⊤

theorem nonempty_preirreducible_inter {α : Type u} [TopologicalSpace α] [PreirreducibleSpace α] {s : Set α} {t : Set α} : IsOpen s → IsOpen t → Set.Nonempty s → Set.Nonempty t → Set.Nonempty (s ∩ t)

theorem IsOpen.dense {α : Type u} [TopologicalSpace α] [PreirreducibleSpace α] {s : Set α} (ho : IsOpen s) (hne : Set.Nonempty s) : Dense s

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

theorem IsPreirreducible.image {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] {s : Set α} (H : IsPreirreducible s) (f : α → β) (hf : ContinuousOn f s) : IsPreirreducible (f '' s)

theorem IsIrreducible.image {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] {s : Set α} (H : IsIrreducible s) (f : α → β) (hf : ContinuousOn f s) : IsIrreducible (f '' s)

theorem Subtype.preirreducibleSpace {α : Type u} [TopologicalSpace α] {s : Set α} (h : IsPreirreducible s) : PreirreducibleSpace ↑s

theorem Subtype.irreducibleSpace {α : Type u} [TopologicalSpace α] {s : Set α} (h : IsIrreducible s) : IrreducibleSpace ↑s

instance instIrreducibleSpaceCofiniteTopologyInstTopologicalSpaceCofiniteTopology {α : Type u_3} [Infinite α] : IrreducibleSpace (CofiniteTopology α)

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

Equations

• @instIrreducibleSpaceCofiniteTopologyInstTopologicalSpaceCofiniteTopology = @instIrreducibleSpaceCofiniteTopologyInstTopologicalSpaceCofiniteTopology.proof_1

theorem isIrreducible_iff_sInter {α : Type u} [TopologicalSpace α] {s : Set α} : IsIrreducible s ↔ ∀ (U : Finset (Set α)), (∀ (u : Set α), u ∈ U → IsOpen u) → (∀ (u : Set α), u ∈ U → Set.Nonempty (s ∩ u)) → Set.Nonempty (s ∩ ⋂₀ ↑U)

A set s is irreducible if and only if for every finite collection of open sets all of whose members intersect s, s also intersects the intersection of the entire collection (i.e., there is an element of s contained in every member of the collection).

theorem isPreirreducible_iff_closed_union_closed {α : Type u} [TopologicalSpace α] {s : Set α} : IsPreirreducible s ↔ ∀ (z₁ z₂ : Set α), IsClosed z₁ → IsClosed z₂ → s ⊆ z₁ ∪ z₂ → s ⊆ z₁ ∨ s ⊆ z₂

A set is preirreducible if and only if for every cover by two closed sets, it is contained in one of the two covering sets.

theorem isIrreducible_iff_sUnion_closed {α : Type u} [TopologicalSpace α] {s : Set α} : IsIrreducible s ↔ ∀ (Z : Finset (Set α)), (∀ (z : Set α), z ∈ Z → IsClosed z) → s ⊆ ⋃₀ ↑Z → ∃ z, 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.

theorem subset_closure_inter_of_isPreirreducible_of_isOpen {α : Type u} [TopologicalSpace α] {S : Set α} {U : Set α} (hS : IsPreirreducible S) (hU : IsOpen U) (h : Set.Nonempty (S ∩ U)) : S ⊆ closure (S ∩ U)

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

theorem IsPreirreducible.subset_irreducible {α : Type u} [TopologicalSpace α] {S : Set α} {U : Set α} {Z : Set α} (hZ : IsPreirreducible Z) (hU : Set.Nonempty U) (hU' : IsOpen U) (h₁ : U ⊆ S) (h₂ : S ⊆ Z) : IsIrreducible S

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

theorem IsPreirreducible.open_subset {α : Type u} [TopologicalSpace α] {Z : Set α} {U : Set α} (hZ : IsPreirreducible Z) (hU : IsOpen U) (hU' : U ⊆ Z) : IsPreirreducible U

theorem IsPreirreducible.interior {α : Type u} [TopologicalSpace α] {Z : Set α} (hZ : IsPreirreducible Z) : IsPreirreducible (interior Z)

theorem IsPreirreducible.preimage {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] {Z : Set α} (hZ : IsPreirreducible Z) {f : β → α} (hf : OpenEmbedding f) : IsPreirreducible (f ⁻¹' Z)