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 {X : Type u} [TopologicalSpace X] (s : Set X) : 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 X⦄ [inst_1 : Filter.NeBot f], f ≤ Filter.principal s → ∃ x ∈ s, ClusterPt x 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 : Set X} {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 : Set X} {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 : Set X} {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 : Set X} {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 : Set X} {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_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_nhds_of_unique_mapClusterPt {X : Type u} {Y : Type v} [TopologicalSpace X] {s : Set X} {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 (x x_1 : Set X) => 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 {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 (_ : ↑x ∈ s) ∈ 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 (_ : ↑x ∈ s)

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.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} [hι : Nonempty ι] (hs : IsCompact s) (t : ι → Set X) (htc : ∀ (i : ι), IsClosed (t i)) (hst : s ∩ ⋂ (i : ι), t i = ∅) (hdt : Directed (fun (x x_1 : Set X) => x ⊇ x_1) 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 LocallyFinite.finite_nonempty_inter_compact {X : Type u} {ι : Type u_1} [TopologicalSpace X] {s : Set X} {f : ι → Set X} (hf : LocallyFinite f) (hs : IsCompact s) : Set.Finite {i : ι | Set.Nonempty (f i ∩ s)}

If s is a compact set in a topological space X and f : ι → Set X is a locally finite family of sets, then f i ∩ s is nonempty only for a finitely many i.

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 ι), Set.Nonempty (s ∩ ⋂ i ∈ u, t i)) : Set.Nonempty (s ∩ ⋂ (i : ι), t 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 {X : Type u} [TopologicalSpace X] {ι : Type v} [hι : Nonempty ι] (t : ι → Set X) (htd : Directed (fun (x x_1 : Set X) => x ⊇ x_1) t) (htn : ∀ (i : ι), Set.Nonempty (t i)) (htc : ∀ (i : ι), IsCompact (t i)) (htcl : ∀ (i : ι), IsClosed (t i)) : Set.Nonempty (⋂ (i : ι), t 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 {X : Type u} [TopologicalSpace X] (t : ℕ → Set X) (htd : ∀ (i : ℕ), t (i + 1) ⊆ t i) (htn : ∀ (i : ℕ), Set.Nonempty (t i)) (ht0 : IsCompact (t 0)) (htcl : ∀ (i : ℕ), IsClosed (t i)) : Set.Nonempty (⋂ (i : ℕ), t 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 {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, 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 {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} {Y : Type v} [TopologicalSpace X] {K : Set X} {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} {Y : Type v} [TopologicalSpace X] {K : Set X} (hK : IsCompact K) (l : Filter Y) : nhdsSet K ×ˢ l = ⨆ x ∈ K, nhds x ×ˢ l

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

theorem IsCompact.mem_prod_nhdsSet_of_forall {X : Type u} {Y : Type v} [TopologicalSpace Y] {K : Set Y} {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.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.

@[simp]

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

@[simp]

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 : Set.Subsingleton s) : IsCompact s

theorem Set.Finite.isCompact_biUnion {X : Type u} {ι : Type u_1} [TopologicalSpace X] {s : Set ι} {f : ι → Set X} (hs : Set.Finite s) (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 : Set.Finite S) (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)

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

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

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

theorem IsCompact.union {X : Type u} [TopologicalSpace X] {s : Set X} {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 (x x_1 : Set X) => x ⊇ x_1) 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_nhd_of_compact for version assuming this.

theorem isCompact_open_iff_eq_finite_iUnion_of_isTopologicalBasis {X : Type u} {ι : Type u_1} [TopologicalSpace X] (b : ι → Set X) (hb : TopologicalSpace.IsTopologicalBasis (Set.range b)) (hb' : ∀ (i : ι), IsCompact (b i)) (U : Set X) : IsCompact U ∧ IsOpen U ↔ ∃ (s : Set ι), Set.Finite s ∧ U = ⋃ i ∈ s, b i

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

def Filter.cocompact (X : Type u_2) [TopologicalSpace X] : Filter X

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

Equations

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

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

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

theorem Filter.mem_cocompact' {X : Type u} [TopologicalSpace X] {s : Set X} : s ∈ Filter.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] : Filter.cocompact X ≤ Filter.cofinite

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

@[simp]

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

theorem Filter.Tendsto.isCompact_insert_range_of_cocompact {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {y : Y} (hf : Filter.Tendsto f (Filter.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 : Filter.Tendsto f Filter.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 : Filter.Tendsto f Filter.atTop (nhds x)) : IsCompact (insert x (Set.range f))

def Filter.coclosedCompact (X : Type u_2) [TopologicalSpace X] : Filter X

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 X = ⨅ (s : Set X), ⨅ (_ : IsClosed s), ⨅ (_ : IsCompact s), Filter.principal sᶜ

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

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

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

theorem Filter.cocompact_le_coclosedCompact {X : Type u} [TopologicalSpace X] : Filter.cocompact X ≤ Filter.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

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' := (_ : Filter.cocompact X ≤ Filter.cofinite) }

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

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 {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (s : Set X) (t : Set Y) : 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 {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.

class CompactSpace (X : Type u_2) [TopologicalSpace X] : Prop

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

• isCompact_univ : IsCompact Set.univ

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

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

Equations

• (_ : CompactSpace 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 cluster_point_of_compact {X : Type u} [TopologicalSpace X] [CompactSpace X] (f : Filter X) [Filter.NeBot f] : ∃ (x : X), ClusterPt x f

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

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 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} {Y : Type v} [TopologicalSpace X] [CompactSpace X] {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.

class NoncompactSpace (X : Type u_2) [TopologicalSpace X] : Prop

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

• noncompact_univ : ¬IsCompact Set.univ

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

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 instNeBotCocompact {X : Type u} [TopologicalSpace X] [NoncompactSpace X] : Filter.NeBot (Filter.cocompact X)

Equations

• (_ : Filter.NeBot (Filter.cocompact X)) = (_ : Filter.NeBot (Filter.cocompact X))

@[simp]

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

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

Equations

• (_ : Filter.NeBot (Filter.coclosedCompact X)) = (_ : Filter.NeBot (Filter.coclosedCompact X))

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

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

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

instance instNoncompactSpaceIntInstTopologicalSpaceInt : NoncompactSpace ℤ

Equations

• instNoncompactSpaceIntInstTopologicalSpaceInt = (_ : 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 : Set X} {K : Set X} (hs : Set.Infinite s) (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 : Set X} {K : Set X} (hs : Set.Infinite s) (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 : Set.Infinite s) : ∃ (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 : Set.Infinite s) : ∃ (x : X), AccPt x (Filter.principal s)

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

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 LocallyFinite.finite_nonempty_of_compact {X : Type u} {ι : Type u_1} [TopologicalSpace X] [CompactSpace X] {f : ι → Set X} (hf : LocallyFinite f) : Set.Finite {i : ι | Set.Nonempty (f i)}

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

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

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

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

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

Equations

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

theorem Filter.comap_cocompact_le {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : Continuous f) : Filter.comap f (Filter.cocompact Y) ≤ Filter.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 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 isCompact_diagonal {X : Type u} [TopologicalSpace X] [CompactSpace X] : IsCompact (Set.diagonal X)

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

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

theorem isClosedMap_fst_of_compactSpace {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] [CompactSpace Y] : IsClosedMap Prod.fst

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

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

theorem Inducing.isCompact_iff {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {s : Set X} {f : X → Y} (hf : Inducing 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 Embedding.isCompact_iff {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {s : Set X} {f : X → Y} (hf : Embedding 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 Inducing.isCompact_preimage {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : Inducing 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 Inducing.isCompact_preimage_iff {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : Inducing f) {K : Set Y} (Kf : K ⊆ Set.range f) : IsCompact (f ⁻¹' K) ↔ IsCompact K

theorem Inducing.isCompact_preimage' {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : Inducing 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 ClosedEmbedding.isCompact_preimage {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : ClosedEmbedding 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 ClosedEmbedding.tendsto_cocompact {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : ClosedEmbedding f) : Filter.Tendsto f (Filter.cocompact X) (Filter.cocompact Y)

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 {X : Type u} [TopologicalSpace X] {p : X → Prop} {s : Set { x : X // p x }} : IsCompact s ↔ IsCompact (Subtype.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_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' : DiscreteTopology ↑s) : Set.Finite s

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

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

theorem ClosedEmbedding.compactSpace {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] [h : CompactSpace Y] {f : X → Y} (hf : ClosedEmbedding 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 Finite.compactSpace {X : Type u} [TopologicalSpace X] [Finite X] : CompactSpace X

Finite topological spaces are compact.

Equations

• (_ : CompactSpace X) = (_ : CompactSpace X)

instance instCompactSpaceProdInstTopologicalSpaceProd {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.

Equations

• (_ : CompactSpace (X × Y)) = (_ : CompactSpace (X × Y))

instance instCompactSpaceSumInstTopologicalSpaceSum {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.

Equations

• (_ : CompactSpace (X ⊕ Y)) = (_ : CompactSpace (X ⊕ Y))

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

Equations

• (_ : CompactSpace ((i : ι) × X i)) = (_ : CompactSpace ((i : ι) × X i))

theorem Filter.coprod_cocompact {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] : Filter.coprod (Filter.cocompact X) (Filter.cocompact Y) = Filter.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 Prod.noncompactSpace_left {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] [NoncompactSpace X] [Nonempty Y] : NoncompactSpace (X × Y)

Equations

• (_ : NoncompactSpace (X × Y)) = (_ : NoncompactSpace (X × Y))

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

Equations

• (_ : NoncompactSpace (X × 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.pi Set.univ 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)

Equations

• (_ : CompactSpace ((i : ι) → X i)) = (_ : CompactSpace ((i : ι) → X i))

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

Equations

• (_ : CompactSpace (ι → Y)) = (_ : CompactSpace (ι → Y))

theorem Filter.coprodᵢ_cocompact {ι : Type u_1} {X : ι → Type u_3} [(d : ι) → TopologicalSpace (X d)] : (Filter.coprodᵢ fun (d : ι) => Filter.cocompact (X d)) = Filter.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)

Equations

• (_ : CompactSpace (Quot r)) = (_ : CompactSpace (Quot r))

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

Equations

• (_ : CompactSpace (Quotient s)) = (_ : CompactSpace (Quot Setoid.r))

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