# 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.
theorem IsCompact.exists_clusterPt {X : Type u} [] {s : Set X} (hs : ) {f : } [f.NeBot] (hf : ) :
xs,
theorem IsCompact.exists_mapClusterPt {X : Type u} [] {s : Set X} {ι : Type u_2} (hs : ) {f : } [f.NeBot] {u : ιX} (hf : ) :
xs, MapClusterPt x f u
theorem IsCompact.compl_mem_sets {X : Type u} [] {s : Set X} (hs : ) {f : } (hf : xs, 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} [] {s : Set X} (hs : ) {f : } (hf : xs, t, 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} [] {s : Set X} (hs : ) {p : Set XProp} (he : p ) (hmono : ∀ ⦃s t : Set X⦄, s tp tp s) (hunion : ∀ ⦃s t : Set X⦄, p sp tp (s t)) (hnhds : xs, t, 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} [] {s : Set X} {t : Set X} (hs : ) (ht : ) :

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

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

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

theorem IsCompact.diff {X : Type u} [] {s : Set X} {t : Set X} (hs : ) (ht : ) :
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} [] {s : Set X} {t : Set X} (hs : ) (ht : ) (h : t s) :

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

theorem IsCompact.image_of_continuousOn {X : Type u} {Y : Type v} [] [] {s : Set X} {f : XY} (hs : ) (hf : ) :
theorem IsCompact.image {X : Type u} {Y : Type v} [] [] {s : Set X} {f : XY} (hs : ) (hf : ) :
theorem IsCompact.adherence_nhdset {X : Type u} [] {s : Set X} {t : Set X} {f : } (hs : ) (hf₂ : ) (ht₁ : ) (ht₂ : xs, x t) :
t f
theorem isCompact_iff_ultrafilter_le_nhds {X : Type u} [] {s : Set X} :
∀ (f : ), xs, f nhds x
theorem IsCompact.ultrafilter_le_nhds {X : Type u} [] {s : Set X} :
∀ (f : ), xs, f nhds x

Alias of the forward direction of isCompact_iff_ultrafilter_le_nhds.

theorem isCompact_iff_ultrafilter_le_nhds' {X : Type u} [] {s : Set X} :
∀ (f : ), s fxs, f nhds x
theorem IsCompact.ultrafilter_le_nhds' {X : Type u} [] {s : Set X} :
∀ (f : ), s fxs, f nhds x

Alias of the forward direction of isCompact_iff_ultrafilter_le_nhds'.

theorem IsCompact.le_nhds_of_unique_clusterPt {X : Type u} [] {s : Set X} (hs : ) {l : } {y : X} (hmem : s l) (h : xs, 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} [] {s : Set X} {Y : Type u_2} {l : } {y : X} {f : YX} (hs : ) (hmem : ∀ᶠ (x : Y) in l, f x s) (h : xs, MapClusterPt x l fx = 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} [] {s : Set X} {ι : Type v} [hι : ] (hs : ) (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} [] {s : Set X} {ι : Type v} (hs : ) (U : ιSet X) (hUo : ∀ (i : ι), IsOpen (U i)) (hsU : s ⋃ (i : ι), U i) :
∃ (t : ), s it, U i

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

theorem IsCompact.elim_nhds_subcover_nhdsSet' {X : Type u} [] {s : Set X} (hs : ) (U : (x : X) → x sSet X) (hU : ∀ (x : X) (hx : x s), U x hx nhds x) :
∃ (t : Finset s), xt, U x
theorem IsCompact.elim_nhds_subcover_nhdsSet {X : Type u} [] {s : Set X} (hs : ) {U : XSet X} (hU : xs, U x nhds x) :
∃ (t : ), (∀ xt, x s) xt, U x
theorem IsCompact.elim_nhds_subcover' {X : Type u} [] {s : Set X} (hs : ) (U : (x : X) → x sSet X) (hU : ∀ (x : X) (hx : x s), U x hx nhds x) :
∃ (t : Finset s), s xt, U x
theorem IsCompact.elim_nhds_subcover {X : Type u} [] {s : Set X} (hs : ) (U : XSet X) (hU : xs, U x nhds x) :
∃ (t : ), (∀ xt, x s) s xt, U x
theorem IsCompact.disjoint_nhdsSet_left {X : Type u} [] {s : Set X} {l : } (hs : ) :
Disjoint (nhdsSet s) l xs, 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} [] {s : Set X} {l : } (hs : ) :
Disjoint l (nhdsSet s) xs, 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} [] {s : Set X} {ι : Type v} [hι : ] (hs : ) (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} [] {s : Set X} {ι : Type v} (hs : ) (t : ιSet X) (htc : ∀ (i : ι), IsClosed (t i)) (hst : s ⋂ (i : ι), t i = ) :
∃ (u : ), s iu, 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} [] {s : Set X} {f : ιSet X} (hf : ) (hs : ) :
{i : ι | (f i s).Nonempty}.Finite

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} [] {s : Set X} {ι : Type v} (hs : ) (t : ιSet X) (htc : ∀ (i : ι), IsClosed (t i)) (hst : ∀ (u : ), (s iu, 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_iInter_of_directed_nonempty_isCompact_isClosed {X : Type u} [] {ι : Type v} [hι : ] (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.

@[deprecated IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed]
theorem IsCompact.nonempty_iInter_of_directed_nonempty_compact_closed {X : Type u} [] {ι : Type v} [hι : ] (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

Alias of IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed.

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} [] {S : Set (Set X)} [hS : Nonempty S] (hSd : DirectedOn (fun (x1 x2 : Set X) => x1 x2) S) (hSn : US, U.Nonempty) (hSc : US, ) (hScl : US, ) :
(⋂₀ 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} [] (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.

@[deprecated IsCompact.nonempty_iInter_of_sequence_nonempty_isCompact_isClosed]
theorem IsCompact.nonempty_iInter_of_sequence_nonempty_compact_closed {X : Type u} [] (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

Alias of IsCompact.nonempty_iInter_of_sequence_nonempty_isCompact_isClosed.

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} [] {s : Set X} {b : Set ι} {c : ιSet X} (hs : ) (hc₁ : ib, IsOpen (c i)) (hc₂ : s ib, c i) :
b'b, b'.Finite s ib', c i

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

theorem isCompact_of_finite_subcover {X : Type u} [] {s : Set X} (h : ∀ {ι : Type u} (U : ιSet X), (∀ (i : ι), IsOpen (U i))s ⋃ (i : ι), U i∃ (t : ), s it, U i) :

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} [] {s : Set X} (h : ∀ {ι : Type u} (t : ιSet X), (∀ (i : ι), IsClosed (t i))s ⋂ (i : ι), t i = ∃ (u : ), s iu, t i = ) :

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} [] {s : Set X} :
∀ {ι : Type u} (U : ιSet X), (∀ (i : ι), IsOpen (U i))s ⋃ (i : ι), U i∃ (t : ), s it, 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} [] {s : Set X} :
∀ {ι : Type u} (t : ιSet X), (∀ (i : ι), IsClosed (t i))s ⋂ (i : ι), t i = ∃ (u : ), s iu, 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} [] {K : Set X} {Y : Type u_2} {l : } {s : Set (X × Y)} (hK : ) (hs : xK, s nhds x ×ˢ l) :
s ×ˢ 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} [] {K : Set X} (hK : ) {Y : Type u_2} (l : ) :
×ˢ l = xK, nhds x ×ˢ l
theorem IsCompact.prod_nhdsSet_eq_biSup {Y : Type v} [] {K : Set Y} (hK : ) {X : Type u_2} (l : ) :
l ×ˢ = yK, l ×ˢ nhds y
theorem IsCompact.mem_prod_nhdsSet_of_forall {Y : Type v} [] {K : Set Y} {X : Type u_2} {l : } {s : Set (X × Y)} (hK : ) (hs : yK, s l ×ˢ nhds y) :
s l ×ˢ

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} [] {K : Set X} (hK : ) (l : ) :
l = xK, nhds x l
theorem IsCompact.inf_nhdsSet_eq_biSup {X : Type u} [] {K : Set X} (hK : ) (l : ) :
l = xK, l nhds x
theorem IsCompact.mem_nhdsSet_inf_of_forall {X : Type u} [] {K : Set X} {l : } {s : Set X} (hK : ) (hs : xK, s nhds x l) :
s 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} [] {K : Set X} {l : } {s : Set X} (hK : ) (hs : yK, s l nhds y) :
s l

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} [] [] {x₀ : X} {K : Set Y} (hK : ) {P : XYProp} (hP : yK, ∀ᶠ (z : X × Y) in nhds (x₀, y), P z.1 z.2) :
∀ᶠ (x : X) in nhds x₀, yK, 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} [] :
@[simp]
theorem isCompact_singleton {X : Type u} [] {x : X} :
theorem Set.Subsingleton.isCompact {X : Type u} [] {s : Set X} (hs : s.Subsingleton) :
theorem Set.Finite.isCompact_biUnion {X : Type u} {ι : Type u_1} [] {s : Set ι} {f : ιSet X} (hs : s.Finite) (hf : is, IsCompact (f i)) :
IsCompact (⋃ is, f i)
theorem Finset.isCompact_biUnion {X : Type u} {ι : Type u_1} [] (s : ) {f : ιSet X} (hf : is, IsCompact (f i)) :
IsCompact (⋃ is, f i)
theorem isCompact_accumulate {X : Type u} [] {K : Set X} (hK : ∀ (n : ), IsCompact (K n)) (n : ) :
theorem Set.Finite.isCompact_sUnion {X : Type u} [] {S : Set (Set X)} (hf : S.Finite) (hc : sS, ) :
theorem isCompact_iUnion {X : Type u} [] {ι : Sort u_2} {f : ιSet X} [] (h : ∀ (i : ι), IsCompact (f i)) :
IsCompact (⋃ (i : ι), f i)
theorem Set.Finite.isCompact {X : Type u} [] {s : Set X} (hs : s.Finite) :
theorem IsCompact.finite_of_discrete {X : Type u} [] {s : Set X} [] (hs : ) :
s.Finite
theorem isCompact_iff_finite {X : Type u} [] {s : Set X} [] :
s.Finite
theorem IsCompact.union {X : Type u} [] {s : Set X} {t : Set X} (hs : ) (ht : ) :
theorem IsCompact.insert {X : Type u} [] {s : Set X} (hs : ) (a : X) :
theorem exists_subset_nhds_of_isCompact' {X : Type u} {ι : Type u_1} [] [] {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_nhd_of_compact for version assuming this.

theorem eq_finite_iUnion_of_isTopologicalBasis_of_isCompact_open {X : Type u} {ι : Type u_1} [] (b : ιSet X) (hb : ) (U : Set X) (hUc : ) (hUo : ) :
∃ (s : Set ι), s.Finite U = is, b i
theorem eq_sUnion_finset_of_isTopologicalBasis_of_isCompact_open {X : Type u} [] (b : Set (Set X)) (U : Set X) (hUc : ) (hUo : ) :
∃ (s : Finset b), U = ⋃₀ (Subtype.val '' s)
theorem isCompact_open_iff_eq_finite_iUnion_of_isTopologicalBasis {X : Type u} {ι : Type u_1} [] (b : ιSet X) (hb : ) (hb' : ∀ (i : ι), IsCompact (b i)) (U : Set X) :
∃ (s : Set ι), s.Finite U = is, 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

theorem Filter.hasBasis_cocompact {X : Type u} [] :
.HasBasis IsCompact compl
theorem Filter.mem_cocompact {X : Type u} [] {s : Set X} :
∃ (t : Set X), t s
theorem Filter.mem_cocompact' {X : Type u} [] {s : Set X} :
∃ (t : Set X), s t
theorem IsCompact.compl_mem_cocompact {X : Type u} [] {s : Set X} (hs : ) :
theorem Filter.cocompact_le_cofinite {X : Type u} [] :
Filter.cofinite
theorem Filter.cocompact_eq_cofinite (X : Type u_2) [] [] :
= Filter.cofinite
theorem Filter.disjoint_cocompact_left {X : Type u} [] (f : ) :
Kf,

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} [] (f : ) :
Kf,

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

@[deprecated]
theorem Nat.cocompact_eq :
= Filter.atTop
theorem Filter.Tendsto.isCompact_insert_range_of_cocompact {X : Type u} {Y : Type v} [] [] {f : XY} {y : Y} (hf : Filter.Tendsto f (nhds y)) (hfc : ) :
theorem Filter.Tendsto.isCompact_insert_range_of_cofinite {X : Type u} {ι : Type u_1} [] {f : ιX} {x : X} (hf : Filter.Tendsto f Filter.cofinite (nhds x)) :
theorem Filter.Tendsto.isCompact_insert_range {X : Type u} [] {f : X} {x : X} (hf : Filter.Tendsto f Filter.atTop (nhds x)) :
theorem Filter.hasBasis_coclosedCompact {X : Type u} [] :
.HasBasis (fun (s : Set X) => ) compl
theorem Filter.mem_coclosedCompact_iff {X : Type u} [] {s : Set X} :

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

@[deprecated Filter.mem_coclosedCompact_iff]
theorem Filter.mem_coclosedCompact {X : Type u} [] {s : Set X} :
∃ (t : Set X), t s
@[deprecated Filter.mem_coclosedCompact_iff]
theorem Filter.mem_coclosed_compact' {X : Type u} [] {s : Set X} :
∃ (t : Set X), s t
theorem Filter.compl_mem_coclosedCompact {X : Type u} [] {s : Set X} :

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

theorem IsCompact.compl_mem_coclosedCompact_of_isClosed {X : Type u} [] {s : Set X} (hs : ) (hs' : ) :
def Bornology.inCompact (X : Type u) [] :

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
• = { cobounded' := , le_cofinite' := }
Instances For
theorem Bornology.inCompact.isBounded_iff {X : Type u} [] {s : Set X} :
∃ (t : Set X), s t
theorem IsCompact.nhdsSet_prod_eq {X : Type u} {Y : Type v} [] [] {s : Set X} {t : Set Y} (hs : ) (ht : ) :

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} [] [] {s : Set X} {f : } (hs : ) (hf : ) :
×ˢ f nhdsSet (s ×ˢ Set.univ)
theorem prod_nhdsSet_le_of_disjoint_cocompact {X : Type u} [] {t : Set X} {f : } (ht : ) (hf : ) :
f ×ˢ nhdsSet (Set.univ ×ˢ t)
theorem generalized_tube_lemma {X : Type u} {Y : Type v} [] [] {s : Set X} (hs : ) {t : Set Y} (ht : ) {n : Set (X × Y)} (hn : ) (hp : s ×ˢ t n) :
∃ (u : Set X) (v : Set Y), 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.

@[instance 10]
instance Subsingleton.compactSpace {X : Type u} [] [] :
Equations
• =
theorem isCompact_univ_iff {X : Type u} [] :
IsCompact Set.univ
theorem isCompact_univ {X : Type u} [] [h : ] :
IsCompact Set.univ
theorem exists_clusterPt_of_compactSpace {X : Type u} [] [] (f : ) [f.NeBot] :
∃ (x : X),
@[deprecated exists_clusterPt_of_compactSpace]
theorem cluster_point_of_compact {X : Type u} [] [] (f : ) [f.NeBot] :
∃ (x : X),

Alias of exists_clusterPt_of_compactSpace.

theorem Ultrafilter.le_nhds_lim {X : Type u} [] [] (F : ) :
F nhds F.lim
theorem CompactSpace.elim_nhds_subcover {X : Type u} [] [] (U : XSet X) (hU : ∀ (x : X), U x nhds x) :
∃ (t : ), xt, U x =
theorem compactSpace_of_finite_subfamily_closed {X : Type u} [] (h : ∀ {ι : Type u} (t : ιSet X), (∀ (i : ι), IsClosed (t i))⋂ (i : ι), t i = ∃ (u : ), iu, t i = ) :
theorem IsClosed.isCompact {X : Type u} [] {s : Set X} [] (h : ) :
theorem le_nhds_of_unique_clusterPt {X : Type u} [] [] {l : } {y : X} (h : ∀ (x : X), 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 u_2} {l : } {y : X} {f : YX} (h : ∀ (x : X), MapClusterPt x l fx = 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) [] [] :
¬IsCompact Set.univ
theorem IsCompact.ne_univ {X : Type u} [] {s : Set X} [] (hs : ) :
s Set.univ
instance instNeBotCocompactOfNoncompactSpace {X : Type u} [] [] :
.NeBot
Equations
• =
@[simp]
theorem Filter.cocompact_eq_bot {X : Type u} [] [] :
instance instNeBotCoclosedCompactOfNoncompactSpace {X : Type u} [] [] :
.NeBot
Equations
• =
theorem noncompactSpace_of_neBot {X : Type u} [] :
.NeBot
theorem Filter.cocompact_neBot_iff {X : Type u} [] :
.NeBot
theorem not_compactSpace_iff {X : Type u} [] :
Equations
theorem finite_of_compact_of_discrete {X : Type u} [] [] [] :

A compact discrete space is finite.

theorem Set.Infinite.exists_accPt_cofinite_inf_principal_of_subset_isCompact {X : Type u} [] {s : Set X} {K : Set X} (hs : s.Infinite) (hK : ) (hsub : s K) :
xK, AccPt x (Filter.cofinite )
theorem Set.Infinite.exists_accPt_of_subset_isCompact {X : Type u} [] {s : Set X} {K : Set X} (hs : s.Infinite) (hK : ) (hsub : s K) :
xK,
theorem Set.Infinite.exists_accPt_cofinite_inf_principal {X : Type u} [] {s : Set X} [] (hs : s.Infinite) :
∃ (x : X), AccPt x (Filter.cofinite )
theorem Set.Infinite.exists_accPt_principal {X : Type u} [] {s : Set X} [] (hs : s.Infinite) :
∃ (x : X),
theorem exists_nhds_ne_neBot (X : Type u_2) [] [] [] :
∃ (z : X), (nhdsWithin z {z}).NeBot
theorem finite_cover_nhds_interior {X : Type u} [] [] {U : XSet X} (hU : ∀ (x : X), U x nhds x) :
∃ (t : ), xt, interior (U x) = Set.univ
theorem finite_cover_nhds {X : Type u} [] [] {U : XSet X} (hU : ∀ (x : X), U x nhds x) :
∃ (t : ), xt, U x = Set.univ
theorem LocallyFinite.finite_nonempty_of_compact {X : Type u} {ι : Type u_1} [] [] {f : ιSet X} (hf : ) :
{i : ι | (f i).Nonempty}.Finite

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} [] [] {f : ιSet X} (hf : ) (hne : ∀ (i : ι), (f i).Nonempty) :
Set.univ.Finite

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} [] [] {f : ιSet X} (hf : ) (hne : ∀ (i : ι), (f i).Nonempty) :

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
• hf.fintypeOfCompact hne =
Instances For
theorem Filter.comap_cocompact_le {X : Type u} {Y : Type v} [] [] {f : XY} (hf : ) :

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} [] [] [] {f : XY} (hf : ) :
theorem isCompact_diagonal {X : Type u} [] [] :
theorem isClosedMap_snd_of_compactSpace {X : Type u} {Y : Type v} [] [] [] :
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} [] [] [] :
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} [] [] [] {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 Inducing.isCompact_iff {X : Type u} {Y : Type v} [] [] {s : Set X} {f : XY} (hf : ) :

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} [] [] {s : Set X} {f : XY} (hf : ) :

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} [] [] {f : XY} (hf : ) (hf' : ) {K : Set Y} (hK : ) :

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} [] [] {f : XY} (hf : ) {K : Set Y} (Kf : K ) :
theorem Inducing.isCompact_preimage' {X : Type u} {Y : Type v} [] [] {f : XY} (hf : ) {K : Set Y} (hK : ) (Kf : 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} [] [] {f : XY} (hf : ) {K : Set Y} (hK : ) :

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

theorem ClosedEmbedding.tendsto_cocompact {X : Type u} {Y : Type v} [] [] {f : XY} (hf : ) :

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} [] {p : XProp} {s : Set { x : X // p x }} :
IsCompact (Subtype.val '' s)

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

theorem isCompact_iff_isCompact_univ {X : Type u} [] {s : Set X} :
IsCompact Set.univ
theorem isCompact_iff_compactSpace {X : Type u} [] {s : Set X} :
theorem IsCompact.finite {X : Type u} [] {s : Set X} (hs : ) (hs' : ) :
s.Finite
theorem exists_nhds_ne_inf_principal_neBot {X : Type u} [] {s : Set X} (hs : ) (hs' : s.Infinite) :
zs, (nhdsWithin z {z} ).NeBot
theorem ClosedEmbedding.noncompactSpace {X : Type u} {Y : Type v} [] [] [] {f : XY} (hf : ) :
theorem ClosedEmbedding.compactSpace {X : Type u} {Y : Type v} [] [] [h : ] {f : XY} (hf : ) :
theorem IsCompact.prod {X : Type u} {Y : Type v} [] [] {s : Set X} {t : Set Y} (hs : ) (ht : ) :
@[instance 100]
instance Finite.compactSpace {X : Type u} [] [] :

Finite topological spaces are compact.

Equations
• =
instance ULift.compactSpace {X : Type u} [] [] :
Equations
• =
instance instCompactSpaceProd {X : Type u} {Y : Type v} [] [] [] [] :

The product of two compact spaces is compact.

Equations
• =
instance instCompactSpaceSum {X : Type u} {Y : Type v} [] [] [] [] :

The disjoint union of two compact spaces is compact.

Equations
• =
instance instCompactSpaceSigmaOfFinite {ι : Type u_1} {X : ιType u_2} [] [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), CompactSpace (X i)] :
CompactSpace ((i : ι) × X i)
Equations
• =
theorem Filter.coprod_cocompact {X : Type u} {Y : Type v} [] [] :
.coprod = 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} [] [] :
@[instance 100]
instance Prod.noncompactSpace_left {X : Type u} {Y : Type v} [] [] [] [] :
Equations
• =
@[instance 100]
instance Prod.noncompactSpace_right {X : Type u} {Y : Type v} [] [] [] [] :
Equations
• =
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)
Equations
• =
instance Function.compactSpace {Y : Type v} {ι : Type u_1} [] [] :
CompactSpace (ιY)
Equations
• =
theorem Pi.isCompact_iff_of_isClosed {ι : Type u_1} {X : ιType u_2} [(i : ι) → TopologicalSpace (X i)] {s : Set ((i : ι) → X i)} (hs : ) :
∀ (i : ι), IsCompact ( '' 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)), s K) ∀ (i : ι), ∃ (Ki : Set (X i)), s ⁻¹' Ki
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} [] {r : XXProp} [] :
Equations
• =
instance Quotient.compactSpace {X : Type u} [] {s : } [] :
Equations
• =
theorem IsClosed.exists_minimal_nonempty_closed_subset {X : Type u} [] [] {S : Set X} (hS : ) (hne : S.Nonempty) :
VS, V.Nonempty V'V, V'.NonemptyIsClosed V'V' = V