Compact sets and compact spaces

Main results

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

• isCompact_generateFrom: Alexander's subbasis theorem - suppose X is a topological space with a subbasis S and s is a subset of X, then s is compact if for any open cover of s with all elements taken from S, there is a finite subcover.

theorem IsCompact.exists_clusterPt {X : Type u} [TopologicalSpace X] {s : Set X} (hs : IsCompact s) {f : Filter X} [f.NeBot] (hf : f ≤ Filter.principal s) : ∃ x ∈ s, ClusterPt x f

theorem IsCompact.exists_mapClusterPt {X : Type u} [TopologicalSpace X] {s : Set X} {ι : Type u_2} (hs : IsCompact s) {f : Filter ι} [f.NeBot] {u : ι → X} (hf : Filter.map u f ≤ Filter.principal s) : ∃ x ∈ s, MapClusterPt x f u

theorem IsCompact.exists_clusterPt_of_frequently {X : Type u} [TopologicalSpace X] {s : Set X} {l : Filter X} (hs : IsCompact s) (hl : ∃ᶠ (x : X) in l, x ∈ s) : ∃ a ∈ s, ClusterPt a l

theorem IsCompact.exists_mapClusterPt_of_frequently {X : Type u} {ι : Type u_1} [TopologicalSpace X] {s : Set X} {l : Filter ι} {f : ι → X} (hs : IsCompact s) (hf : ∃ᶠ (x : ι) in l, f x ∈ s) : ∃ a ∈ s, MapClusterPt a l f

theorem IsCompact.compl_mem_sets {X : Type u} [TopologicalSpace X] {s : Set X} (hs : IsCompact s) {f : Filter X} (hf : ∀ x ∈ s, sᶜ ∈ nhds x ⊓ f) : sᶜ ∈ f

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

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

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

theorem IsCompact.induction_on {X : Type u} [TopologicalSpace X] {s : Set X} (hs : IsCompact s) {p : Set X → Prop} (he : p ∅) (hmono : ∀ ⦃s t : Set X⦄, s ⊆ t → p t → p s) (hunion : ∀ ⦃s t : Set X⦄, p s → p t → p (s ∪ t)) (hnhds : ∀ x ∈ s, ∃ t ∈ nhdsWithin x s, p t) : p s

If p : Set X → 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 {X : Type u} [TopologicalSpace X] {s t : Set X} (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 {X : Type u} [TopologicalSpace X] {s t : Set X} (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 {X : Type u} [TopologicalSpace X] {s t : Set X} (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 {X : Type u} [TopologicalSpace X] {s t : Set X} (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 {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {s : Set X} {f : X → Y} (hs : IsCompact s) (hf : ContinuousOn f s) : IsCompact (f '' s)

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

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

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

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

Alias of the forward direction of isCompact_iff_ultrafilter_le_nhds.

theorem isCompact_iff_ultrafilter_le_nhds' {X : Type u} [TopologicalSpace X] {s : Set X} : IsCompact s ↔ ∀ (f : Ultrafilter X), s ∈ f → ∃ x ∈ s, ↑f ≤ nhds x

theorem IsCompact.ultrafilter_le_nhds' {X : Type u} [TopologicalSpace X] {s : Set X} : IsCompact s → ∀ (f : Ultrafilter X), s ∈ f → ∃ x ∈ s, ↑f ≤ nhds x

Alias of the forward direction of isCompact_iff_ultrafilter_le_nhds'.

theorem IsCompact.le_nhdsSet_of_clusterPt {X : Type u} [TopologicalSpace X] {s : Set X} (hs : IsCompact s) {l : Filter X} {s' : Set X} (hmem : s ∈ l) (h : ∀ x ∈ s, ClusterPt x l → x ∈ s') : l ≤ nhdsSet s'

If a compact set belongs to a filter and all cluster points in this set and in the filter lie in a set s' then the filter is less than or equal to 𝓝ˢ s'.

theorem IsCompact.le_nhds_of_unique_clusterPt {X : Type u} [TopologicalSpace X] {s : Set X} (hs : IsCompact s) {l : Filter X} {y : X} (hmem : s ∈ l) (h : ∀ x ∈ s, ClusterPt x l → x = y) : l ≤ nhds y

If a compact set belongs to a filter and this filter has a unique cluster point y in this set, then the filter is less than or equal to 𝓝 y.

theorem IsCompact.tendsto_nhdsSet_of_mapClusterPt {X : Type u} [TopologicalSpace X] {s : Set X} {Y : Type u_2} {l : Filter Y} {s' : Set X} {f : Y → X} (hs : IsCompact s) (hmem : ∀ᶠ (x : Y) in l, f x ∈ s) (h : ∀ x ∈ s, MapClusterPt x l f → x ∈ s') : Filter.Tendsto f l (nhdsSet s')

If values of f : Y → X belong to a compact set s eventually along a filter l and s' is the set of MapClusterPt for f along l in s, then f tends to 𝓝ˢ s' along l.

theorem IsCompact.tendsto_nhds_of_unique_mapClusterPt {X : Type u} [TopologicalSpace X] {s : Set X} {Y : Type u_2} {l : Filter Y} {y : X} {f : Y → X} (hs : IsCompact s) (hmem : ∀ᶠ (x : Y) in l, f x ∈ s) (h : ∀ x ∈ s, MapClusterPt x l f → x = y) : Filter.Tendsto f l (nhds y)

If values of f : Y → X belong to a compact set s eventually along a filter l and y is a unique MapClusterPt for f along l in s, then f tends to 𝓝 y along l.

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

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

theorem IsCompact.elim_nhds_subcover_nhdsSet' {X : Type u} [TopologicalSpace X] {s : Set X} (hs : IsCompact s) (U : (x : X) → x ∈ s → Set X) (hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ nhds x) : ∃ (t : Finset ↑s), ⋃ x ∈ t, U ↑x ⋯ ∈ nhdsSet s

theorem IsCompact.elim_nhds_subcover_nhdsSet {X : Type u} [TopologicalSpace X] {s : Set X} (hs : IsCompact s) {U : X → Set X} (hU : ∀ x ∈ s, U x ∈ nhds x) : ∃ (t : Finset X), (∀ x ∈ t, x ∈ s) ∧ ⋃ x ∈ t, U x ∈ nhdsSet s

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

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

theorem IsCompact.elim_nhdsWithin_subcover' {X : Type u} [TopologicalSpace X] {s : Set X} (hs : IsCompact s) (U : (x : X) → x ∈ s → Set X) (hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ nhdsWithin x s) : ∃ (t : Finset ↑s), s ⊆ ⋃ x ∈ t, U ↑x ⋯

theorem IsCompact.elim_nhdsWithin_subcover {X : Type u} [TopologicalSpace X] {s : Set X} (hs : IsCompact s) (U : X → Set X) (hU : ∀ x ∈ s, U x ∈ nhdsWithin x s) : ∃ (t : Finset X), (∀ x ∈ t, x ∈ s) ∧ s ⊆ ⋃ x ∈ t, U x

theorem IsCompact.disjoint_nhdsSet_left {X : Type u} [TopologicalSpace X] {s : Set X} {l : Filter X} (hs : IsCompact s) : Disjoint (nhdsSet s) l ↔ ∀ 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 {X : Type u} [TopologicalSpace X] {s : Set X} {l : Filter X} (hs : IsCompact s) : Disjoint l (nhdsSet s) ↔ ∀ 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 {X : Type u} [TopologicalSpace X] {s : Set X} {ι : Type v} [Nonempty ι] (hs : IsCompact s) (t : ι → Set X) (htc : ∀ (i : ι), IsClosed (t i)) (hst : s ∩ ⋂ (i : ι), t i = ∅) (hdt : Directed (fun (x1 x2 : Set X) => x1 ⊇ x2) t) : ∃ (i : ι), s ∩ t 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 {X : Type u} [TopologicalSpace X] {s : Set X} {ι : Type v} (hs : IsCompact s) (t : ι → Set X) (htc : ∀ (i : ι), IsClosed (t i)) (hst : s ∩ ⋂ (i : ι), t i = ∅) : ∃ (u : Finset ι), s ∩ ⋂ i ∈ u, t 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 IsCompact.inter_iInter_nonempty {X : Type u} [TopologicalSpace X] {s : Set X} {ι : Type v} (hs : IsCompact s) (t : ι → Set X) (htc : ∀ (i : ι), IsClosed (t i)) (hst : ∀ (u : Finset ι), (s ∩ ⋂ i ∈ u, t i).Nonempty) : (s ∩ ⋂ (i : ι), t i).Nonempty

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

theorem IsCompact.nonempty_inter_sInter {X : Type u} [TopologicalSpace X] {s : Set X} (hs : IsCompact s) {t : Set (Set X)} (ht : ∀ a ∈ t, IsClosed a) (h : ∀ a ⊆ t, a.Finite → (s ∩ ⋂₀ a).Nonempty) : (s ∩ ⋂₀ t).Nonempty

theorem CompactSpace.nonempty_sInter {X : Type u} [TopologicalSpace X] [CompactSpace X] {s : Set (Set X)} (hsc : ∀ t ∈ s, IsClosed t) (hs : ∀ t ⊆ s, t.Finite → (⋂₀ t).Nonempty) : (⋂₀ s).Nonempty

theorem IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed {X : Type u} [TopologicalSpace X] {ι : Type v} [hι : Nonempty ι] (t : ι → Set X) (htd : Directed (fun (x1 x2 : Set X) => x1 ⊇ x2) t) (htn : ∀ (i : ι), (t i).Nonempty) (htc : ∀ (i : ι), IsCompact (t i)) (htcl : ∀ (i : ι), IsClosed (t i)) : (⋂ (i : ι), t i).Nonempty

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

theorem IsCompact.nonempty_sInter_of_directed_nonempty_isCompact_isClosed {X : Type u} [TopologicalSpace X] {S : Set (Set X)} [hS : Nonempty ↑S] (hSd : DirectedOn (fun (x1 x2 : Set X) => x1 ⊇ x2) S) (hSn : ∀ U ∈ S, U.Nonempty) (hSc : ∀ U ∈ S, IsCompact U) (hScl : ∀ U ∈ S, IsClosed U) : (⋂₀ S).Nonempty

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

theorem IsCompact.nonempty_iInter_of_sequence_nonempty_isCompact_isClosed {X : Type u} [TopologicalSpace X] (t : ℕ → Set X) (htd : ∀ (i : ℕ), t (i + 1) ⊆ t i) (htn : ∀ (i : ℕ), (t i).Nonempty) (ht0 : IsCompact (t 0)) (htcl : ∀ (i : ℕ), IsClosed (t i)) : (⋂ (i : ℕ), t i).Nonempty

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 {X : Type u} {ι : Type u_1} [TopologicalSpace X] {s : Set X} {b : Set ι} {c : ι → Set X} (hs : IsCompact s) (hc₁ : ∀ i ∈ b, IsOpen (c i)) (hc₂ : s ⊆ ⋃ i ∈ b, c i) : ∃ b' ⊆ b, b'.Finite ∧ s ⊆ ⋃ i ∈ b', c i

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

theorem isCompact_of_finite_subcover {X : Type u} [TopologicalSpace X] {s : Set X} (h : ∀ {ι : Type u} (U : ι → Set X), (∀ (i : ι), IsOpen (U i)) → s ⊆ ⋃ (i : ι), U i → ∃ (t : Finset ι), 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 {X : Type u} [TopologicalSpace X] {s : Set X} (h : ∀ {ι : Type u} (t : ι → Set X), (∀ (i : ι), IsClosed (t i)) → s ∩ ⋂ (i : ι), t i = ∅ → ∃ (u : Finset ι), s ∩ ⋂ i ∈ u, t 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 {X : Type u} [TopologicalSpace X] {s : Set X} : IsCompact s ↔ ∀ {ι : Type u} (U : ι → Set X), (∀ (i : ι), IsOpen (U i)) → s ⊆ ⋃ (i : ι), U i → ∃ (t : Finset ι), 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 {X : Type u} [TopologicalSpace X] {s : Set X} : IsCompact s ↔ ∀ {ι : Type u} (t : ι → Set X), (∀ (i : ι), IsClosed (t i)) → s ∩ ⋂ (i : ι), t i = ∅ → ∃ (u : Finset ι), s ∩ ⋂ i ∈ u, t 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 {X : Type u} [TopologicalSpace X] {K : Set X} {Y : Type u_2} {l : Filter Y} {s : Set (X × Y)} (hK : IsCompact K) (hs : ∀ x ∈ K, s ∈ nhds x ×ˢ l) : s ∈ nhdsSet K ×ˢ l

If s : Set (X × Y) 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 {X : Type u} [TopologicalSpace X] {K : Set X} (hK : IsCompact K) {Y : Type u_2} (l : Filter Y) : nhdsSet K ×ˢ l = ⨆ x ∈ K, nhds x ×ˢ l

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

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

If s : Set (X × Y) 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.nhdsSet_inf_eq_biSup {X : Type u} [TopologicalSpace X] {K : Set X} (hK : IsCompact K) (l : Filter X) : nhdsSet K ⊓ l = ⨆ x ∈ K, nhds x ⊓ l

theorem IsCompact.inf_nhdsSet_eq_biSup {X : Type u} [TopologicalSpace X] {K : Set X} (hK : IsCompact K) (l : Filter X) : l ⊓ nhdsSet K = ⨆ x ∈ K, l ⊓ nhds x

theorem IsCompact.mem_nhdsSet_inf_of_forall {X : Type u} [TopologicalSpace X] {K : Set X} {l : Filter X} {s : Set X} (hK : IsCompact K) (hs : ∀ x ∈ K, s ∈ nhds x ⊓ l) : s ∈ nhdsSet K ⊓ l

If s : Set X 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.mem_inf_nhdsSet_of_forall {X : Type u} [TopologicalSpace X] {K : Set X} {l : Filter X} {s : Set X} (hK : IsCompact K) (hs : ∀ y ∈ K, s ∈ l ⊓ nhds y) : s ∈ l ⊓ nhdsSet K

If s : Set S belongs to l ⊓ 𝓝 x for all x 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 {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {x₀ : X} {K : Set Y} (hK : IsCompact K) {P : X → Y → Prop} (hP : ∀ y ∈ K, ∀ᶠ (z : X × Y) in nhds (x₀, y), P z.1 z.2) : ∀ᶠ (x : X) in nhds x₀, ∀ 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.

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

theorem isCompact_singleton {X : Type u} [TopologicalSpace X] {x : X} : IsCompact {x}

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

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

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

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

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

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

@[simp]

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

@[simp]

theorem Set.sUnion_isCompact_eq_univ {X : Type u} [TopologicalSpace X] : ⋃₀ {s : Set X | IsCompact s} = univ

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

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

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

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

theorem exists_subset_nhds_of_isCompact' {X : Type u} {ι : Type u_1} [TopologicalSpace X] [Nonempty ι] {V : ι → Set X} (hV : Directed (fun (x1 x2 : Set X) => x1 ⊇ x2) V) (hV_cpct : ∀ (i : ι), IsCompact (V i)) (hV_closed : ∀ (i : ι), IsClosed (V i)) {U : Set X} (hU : ∀ x ∈ ⋂ (i : ι), V i, U ∈ nhds x) : ∃ (i : ι), V i ⊆ U

If V : ι → Set X 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 X is not assumed to be Hausdorff. See exists_subset_nhds_of_compact for version assuming this.

theorem isCompact_generateFrom {X : Type u} [T : TopologicalSpace X] {S : Set (Set X)} (hTS : T = TopologicalSpace.generateFrom S) {s : Set X} (h : ∀ P ⊆ S, s ⊆ ⋃₀ P → ∃ Q ⊆ P, Q.Finite ∧ s ⊆ ⋃₀ Q) : IsCompact s

Alexander's subbasis theorem. Suppose X is a topological space with a subbasis S and s is a subset of X. Then s is compact if for any open cover of s with all elements taken from S, there is a finite subcover.

theorem isCompact_generateFrom' {X : Type u} [T : TopologicalSpace X] {S : Set (Set X)} (hTS : T = TopologicalSpace.generateFrom S) {s : Set X} (h : ∀ (ι : Type u) (U : ι → ↑S), s ⊆ ⋃ (i : ι), ↑(U i) → ∃ (J : Set ι), J.Finite ∧ s ⊆ ⋃ i ∈ J, ↑(U i)) : IsCompact s

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

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

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

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

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

theorem Filter.cocompact_eq_cofinite (X : Type u_2) [TopologicalSpace X] [DiscreteTopology X] : cocompact X = cofinite

theorem Filter.disjoint_cocompact_left {X : Type u} [TopologicalSpace X] (f : Filter X) : Disjoint (cocompact X) f ↔ ∃ K ∈ f, IsCompact K

A filter is disjoint from the cocompact filter if and only if it contains a compact set.

theorem Filter.disjoint_cocompact_right {X : Type u} [TopologicalSpace X] (f : Filter X) : Disjoint f (cocompact X) ↔ ∃ K ∈ f, IsCompact K

A filter is disjoint from the cocompact filter if and only if it contains a compact set.

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

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

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

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

theorem Filter.mem_coclosedCompact_iff {X : Type u} [TopologicalSpace X] {s : Set X} : s ∈ coclosedCompact X ↔ IsCompact (closure sᶜ)

A set belongs to coclosedCompact if and only if the closure of its complement is compact.

theorem Filter.compl_mem_coclosedCompact {X : Type u} [TopologicalSpace X] {s : Set X} : sᶜ ∈ coclosedCompact X ↔ IsCompact (closure s)

Complement of a set belongs to coclosedCompact if and only if its closure is compact.

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

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

@[implicit_reducible]

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

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 X = { cobounded := Filter.cocompact X, le_cofinite := ⋯ }

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

theorem Bornology.isBounded_image_of_isLocallyBounded_of_isCompact {X : Type u} [TopologicalSpace X] {Y : Type u_2} [Bornology Y] {s : Set X} (hs : IsCompact s) {f : X → Y} (hf : ∀ (x : X), ∃ t ∈ nhds x, IsBounded (f '' t)) : IsBounded (f '' s)

A locally bounded function maps a compact set to a bounded set.

theorem IsCompact.nhdsSet_prod_eq {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {s : Set X} {t : Set Y} (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_of_disjoint_cocompact {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {s : Set X} {f : Filter Y} (hs : IsCompact s) (hf : Disjoint f (Filter.cocompact Y)) : nhdsSet s ×ˢ f ≤ nhdsSet (s ×ˢ Set.univ)

theorem prod_nhdsSet_le_of_disjoint_cocompact {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {t : Set Y} {f : Filter X} (ht : IsCompact t) (hf : Disjoint f (Filter.cocompact X)) : f ×ˢ nhdsSet t ≤ nhdsSet (Set.univ ×ˢ t)

theorem nhds_prod_le_of_disjoint_cocompact {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f : Filter Y} (x : X) (hf : Disjoint f (Filter.cocompact Y)) : nhds x ×ˢ f ≤ nhdsSet ({x} ×ˢ Set.univ)

theorem prod_nhds_le_of_disjoint_cocompact {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f : Filter X} (y : Y) (hf : Disjoint f (Filter.cocompact X)) : f ×ˢ nhds y ≤ nhdsSet (Set.univ ×ˢ {y})

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

theorem IsCompact.nhdsSetWithin_prod_eq {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {s s' : Set X} {t t' : Set Y} (hs : IsCompact s) (ht : IsCompact t) : nhdsSetWithin (s ×ˢ t) (s' ×ˢ t') = nhdsSetWithin s s' ×ˢ nhdsSetWithin t t'

A relative version of IsCompact.nhdsSet_prod_eq: if s and t are compact sets, then the neighborhoods filter of s ×ˢ t within s' ×ˢ t' is the product of the neighborhoods filters of s and t within s' and t'.

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

theorem generalized_tube_lemma' {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {s s' : Set X} (hs : IsCompact s) {t t' : Set Y} (ht : IsCompact t) {n : Set (X × Y)} (hn : n ∈ nhdsSetWithin (s ×ˢ t) (s' ×ˢ t')) : ∃ u ∈ nhdsSetWithin s s', ∃ v ∈ nhdsSetWithin t t', u ×ˢ v ⊆ n

A variant of generalized_tube_lemma in terms of nhdsSetWithin.

theorem generalized_tube_lemma_left {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {s s' : Set X} (hs : IsCompact s) {t : Set Y} (ht : IsCompact t) {n : Set (X × Y)} (hn : n ∈ nhdsSetWithin (s ×ˢ t) (s' ×ˢ t)) : ∃ u ∈ nhdsSetWithin s s', u ×ˢ t ⊆ n

A variant of generalized_tube_lemma that only replaces the set in one direction.

theorem generalized_tube_lemma_right {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {s : Set X} (hs : IsCompact s) {t t' : Set Y} (ht : IsCompact t) {n : Set (X × Y)} (hn : n ∈ nhdsSetWithin (s ×ˢ t) (s ×ˢ t')) : ∃ u ∈ nhdsSetWithin t t', s ×ˢ u ⊆ n

A variant of generalized_tube_lemma that only replaces the set in one direction.

@[instance 10]

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

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

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

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

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

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

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

theorem CompactSpace.iInter_nonempty {X : Type u} [TopologicalSpace X] {ι : Type v} [CompactSpace X] {t : ι → Set X} (htc : ∀ (i : ι), IsClosed (t i)) (hst : ∀ (s : Finset ι), (⋂ i ∈ s, t i).Nonempty) : (⋂ (i : ι), t i).Nonempty

Given a family of closed sets t i in a compact space, if they satisfy the Finite Intersection Property, then the intersection of all t i is nonempty.

theorem compactSpace_generateFrom {X : Type u} [T : TopologicalSpace X] {S : Set (Set X)} (hTS : T = TopologicalSpace.generateFrom S) (h : ∀ P ⊆ S, ⋃₀ P = Set.univ → ∃ Q ⊆ P, Q.Finite ∧ ⋃₀ Q = Set.univ) : CompactSpace X

The CompactSpace version of Alexander's subbasis theorem. If X is a topological space with a subbasis S, then X is compact if for any open cover of X all of whose elements belong to S, there is a finite subcover.

theorem compactSpace_generateFrom' {X : Type u} [T : TopologicalSpace X] {S : Set (Set X)} (hTS : T = TopologicalSpace.generateFrom S) (h : ∀ (ι : Type u) (U : ι → ↑S), ⋃ (i : ι), ↑(U i) = Set.univ → ∃ (J : Set ι), J.Finite ∧ ⋃ i ∈ J, ↑(U i) = Set.univ) : CompactSpace X

theorem compactSpace_generateFrom_of_compl_mem {X : Type u} [T : TopologicalSpace X] (𝔅 : Set (Set X)) (hT : T = TopologicalSpace.generateFrom 𝔅) (h𝔅 : ∀ s ∈ 𝔅, sᶜ ∈ 𝔅) (h : ∀ P ⊆ 𝔅, (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) → (⋂₀ P).Nonempty) : CompactSpace X

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

theorem le_nhds_of_unique_clusterPt {X : Type u} [TopologicalSpace X] [CompactSpace X] {l : Filter X} {y : X} (h : ∀ (x : X), ClusterPt x l → x = y) : l ≤ nhds y

If a filter has a unique cluster point y in a compact topological space, then the filter is less than or equal to 𝓝 y.

theorem tendsto_nhds_of_unique_mapClusterPt {X : Type u} [TopologicalSpace X] [CompactSpace X] {Y : Type u_2} {l : Filter Y} {y : X} {f : Y → X} (h : ∀ (x : X), MapClusterPt x l f → x = y) : Filter.Tendsto f l (nhds y)

If y is a unique MapClusterPt for f along l and the codomain of f is a compact space, then f tends to 𝓝 y along l.

theorem noncompact_univ (X : Type u_2) [TopologicalSpace X] [NoncompactSpace X] : ¬IsCompact Set.univ

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

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

@[simp]

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

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

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

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

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

instance instNoncompactSpaceInt : NoncompactSpace ℤ

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

A compact discrete space is finite.

theorem Set.Infinite.exists_accPt_cofinite_inf_principal_of_subset_isCompact {X : Type u} [TopologicalSpace X] {s K : Set X} (hs : s.Infinite) (hK : IsCompact K) (hsub : s ⊆ K) : ∃ x ∈ K, AccPt x (Filter.cofinite ⊓ Filter.principal s)

theorem Set.Infinite.exists_accPt_of_subset_isCompact {X : Type u} [TopologicalSpace X] {s K : Set X} (hs : s.Infinite) (hK : IsCompact K) (hsub : s ⊆ K) : ∃ x ∈ K, AccPt x (Filter.principal s)

theorem Set.Infinite.exists_accPt_cofinite_inf_principal {X : Type u} [TopologicalSpace X] {s : Set X} [CompactSpace X] (hs : s.Infinite) : ∃ (x : X), AccPt x (Filter.cofinite ⊓ Filter.principal s)

theorem Set.Infinite.exists_accPt_principal {X : Type u} [TopologicalSpace X] {s : Set X} [CompactSpace X] (hs : s.Infinite) : ∃ (x : X), AccPt x (Filter.principal s)

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

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

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

theorem Filter.comap_cocompact_le {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : Continuous f) : comap f (cocompact Y) ≤ cocompact X

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

theorem disjoint_map_cocompact {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {g : X → Y} {f : Filter X} (hg : Continuous g) (hf : Disjoint f (Filter.cocompact X)) : Disjoint (Filter.map g f) (Filter.cocompact Y)

If a filter is disjoint from the cocompact filter, so is its image under any continuous function.

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

theorem Function.Surjective.compactSpace {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : Continuous f) [CompactSpace X] (hf' : Surjective f) : CompactSpace Y

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

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

theorem Topology.IsInducing.isCompact_iff {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {s : Set X} {f : X → Y} (hf : IsInducing f) : IsCompact s ↔ IsCompact (f '' s)

If f : X → Y is an inducing map, the image f '' s of a set s is compact if and only if s is compact.

theorem Topology.IsEmbedding.isCompact_iff {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {s : Set X} {f : X → Y} (hf : IsEmbedding f) : IsCompact s ↔ IsCompact (f '' s)

If f : X → Y is an embedding, the image f '' s of a set s is compact if and only if s is compact.

theorem Topology.IsInducing.isCompact_preimage {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : IsInducing f) (hf' : IsClosed (Set.range f)) {K : Set Y} (hK : IsCompact K) : IsCompact (f ⁻¹' K)

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

theorem Topology.IsInducing.isCompact_preimage_iff {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : IsInducing f) {K : Set Y} (Kf : K ⊆ Set.range f) : IsCompact (f ⁻¹' K) ↔ IsCompact K

theorem Topology.IsInducing.isCompact_preimage' {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : IsInducing f) {K : Set Y} (hK : IsCompact K) (Kf : K ⊆ Set.range f) : IsCompact (f ⁻¹' K)

The preimage of a compact set in the image of an inducing map is compact.

theorem Topology.IsClosedEmbedding.isCompact_preimage {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : IsClosedEmbedding f) {K : Set Y} (hK : IsCompact K) : IsCompact (f ⁻¹' K)

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

theorem Topology.IsClosedEmbedding.tendsto_cocompact {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : IsClosedEmbedding f) : Filter.Tendsto f (Filter.cocompact X) (Filter.cocompact Y)

A closed embedding is proper, i.e., inverse images of compact sets are contained in compacts. Moreover, the preimage of a compact set is compact, see IsClosedEmbedding.isCompact_preimage.

theorem Subtype.isCompact_iff {X : Type u} [TopologicalSpace X] {p : X → Prop} {s : Set { x : X // p x }} : IsCompact s ↔ IsCompact (val '' s)

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

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

theorem IsCompact.elim_finite_subfamily_isClosed_subtype {X : Type u_2} [TopologicalSpace X] {s : Set X} (ks : IsCompact s) {ι : Type u_3} (t : ι → Set X) {I : Set ι} (htc : ∀ i ∈ I, IsClosed (Subtype.val ⁻¹' t i)) (hst : s ∩ ⋂ i ∈ I, t i = ∅) : ∃ (u : Finset ↑I), s ∩ ⋂ i ∈ u, t ↑i = ∅

An elimination theorem for empty intersections of a family of sets in a compact subset which are closed in the compact subset but not necessarily in the ambient space.

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

theorem IsCompact.finite {X : Type u} [TopologicalSpace X] {s : Set X} (hs : IsCompact s) (hs' : IsDiscrete s) : s.Finite

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

theorem Topology.IsClosedEmbedding.noncompactSpace {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] [NoncompactSpace X] {f : X → Y} (hf : IsClosedEmbedding f) : NoncompactSpace Y

theorem Topology.IsClosedEmbedding.compactSpace {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] [h : CompactSpace Y] {f : X → Y} (hf : IsClosedEmbedding f) : CompactSpace X

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

@[instance 100]

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

Finite topological spaces are compact.

@[instance 100]

instance instCompactSpace {X : Type u} [TopologicalSpace X] [IndiscreteTopology X] : CompactSpace X

The indiscrete topology is compact

instance ULift.compactSpace {X : Type u} [TopologicalSpace X] [CompactSpace X] : CompactSpace (ULift.{v, u} X)

instance instCompactSpaceProd {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] [CompactSpace X] [CompactSpace Y] : CompactSpace (X × Y)

The product of two compact spaces is compact.

instance instCompactSpaceSum {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] [CompactSpace X] [CompactSpace Y] : CompactSpace (X ⊕ Y)

The disjoint union of two compact spaces is compact.

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

theorem Set.isCompact_sigma {ι : Type u_1} {X : ι → Type u_2} [(i : ι) → TopologicalSpace (X i)] {s : Set ι} {t : (i : ι) → Set (X i)} (hs : s.Finite) (ht : ∀ i ∈ s, IsCompact (t i)) : IsCompact (s.sigma t)

theorem IsCompact.sigma_exists_finite_sigma_eq {ι : Type u_1} {X : ι → Type u_2} [(i : ι) → TopologicalSpace (X i)] (u : Set ((i : ι) × X i)) (hu : IsCompact u) : ∃ (s : Set ι) (t : (i : ι) → Set (X i)), s.Finite ∧ (∀ (i : ι), IsCompact (t i)) ∧ s.sigma t = u

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

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

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

@[instance 100]

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

@[instance 100]

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

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

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

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

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

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

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

theorem Pi.isCompact_iff_of_isClosed {ι : Type u_1} {X : ι → Type u_2} [(i : ι) → TopologicalSpace (X i)] {s : Set ((i : ι) → X i)} (hs : IsClosed s) : IsCompact s ↔ ∀ (i : ι), IsCompact (Function.eval i '' s)

theorem Pi.exists_compact_superset_iff {ι : Type u_1} {X : ι → Type u_2} [(i : ι) → TopologicalSpace (X i)] {s : Set ((i : ι) → X i)} : (∃ (K : Set ((i : ι) → X i)), IsCompact K ∧ s ⊆ K) ↔ ∀ (i : ι), ∃ (Ki : Set (X i)), IsCompact Ki ∧ s ⊆ Function.eval i ⁻¹' Ki

theorem Filter.coprodᵢ_cocompact {ι : Type u_1} {X : ι → Type u_3} [(d : ι) → TopologicalSpace (X d)] : (Filter.coprodᵢ fun (d : ι) => cocompact (X d)) = cocompact ((d : ι) → X d)

Tychonoff's theorem formulated in terms of filters: Filter.cocompact on an indexed product type Π d, X d the Filter.coprodᵢ of filters Filter.cocompact on X d.

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

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

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