Compact sets and compact spaces

Main definitions

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

• IsCompact: a set such that 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.
• CompactSpace: typeclass stating that the whole space is a compact set.
• NoncompactSpace: a space that is not a compact space.

Main results

• isCompact_univ_pi: Tychonov's theorem - an arbitrary product of compact sets is compact.

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_1 : 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 ∈ 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 ∈ 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 ∈ 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 ∈ 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 ∈ 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 ∈ b, c i) : ∃ b', b' ⊆ b ∧ Set.Finite b' ∧ s ⊆ ⋃ 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 ∈ 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 ∈ 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 ∈ 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 ∈ 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 ∈ 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 ∈ 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.1 z.2) : ∀ᶠ (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 ∈ 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 ∈ 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 ∈ 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, ⨅ (_ : 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, ⨅ (_ : 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 ∈ 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 ∈ 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 ∈ t, interior (U x) = Set.univ

theorem finite_cover_nhds {α : Type u} [TopologicalSpace α] [CompactSpace α] {U : α → Set α} (hU : ∀ (x : α), U x ∈ nhds x) : ∃ t, ⋃ 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 s ↔ IsCompact (f '' 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 {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] {s : Set α} {f : α → β} (hf : Embedding f) : IsCompact s ↔ IsCompact (f '' s)

If f : α → β is an Embedding, the image f '' s of a set s is compact if and only if 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 Subtype.isCompact_iff {α : Type u} [TopologicalSpace α] {p : α → Prop} {s : Set { a // p a }} : IsCompact s ↔ IsCompact (Subtype.val '' s)

Sets of subtype are compact iff the image under a coercion is.

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

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