Documentation

Mathlib.Topology.Compactness.Compact

Compact sets and compact spaces #

Main definitions #

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

Main results #

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

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) :

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) :

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 : XY} (hs : IsCompact s) (hf : ContinuousOn f s) :
theorem IsCompact.image {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {s : Set X} {f : XY} (hs : IsCompact s) (hf : Continuous f) :
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₂ : xs, ClusterPt x fx 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 sxs, f nhds x
theorem IsCompact.ultrafilter_le_nhds {X : Type u} [TopologicalSpace X] {s : Set X} :
IsCompact s∀ (f : Ultrafilter X), f Filter.principal sxs, 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 fxs, f nhds x
theorem IsCompact.ultrafilter_le_nhds' {X : Type u} [TopologicalSpace X] {s : Set X} :
IsCompact s∀ (f : Ultrafilter X), 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} [TopologicalSpace X] {s : Set X} (hs : IsCompact s) {l : Filter X} {y : X} (hmem : s l) (h : xs, ClusterPt x lx = 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} [TopologicalSpace X] {s : Set X} {Y : Type u_2} {l : Filter Y} {y : X} {f : YX} (hs : IsCompact s) (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} [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 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} [TopologicalSpace X] {s : Set X} (hs : IsCompact s) (U : (x : X) → x sSet X) (hU : ∀ (x : X) (hx : x s), U x hx nhds x) :
∃ (t : Finset s), xt, U x nhdsSet s
theorem IsCompact.elim_nhds_subcover_nhdsSet {X : Type u} [TopologicalSpace X] {s : Set X} (hs : IsCompact s) {U : XSet X} (hU : xs, U x nhds x) :
∃ (t : Finset X), (∀ xt, x s) xt, U x nhdsSet s
theorem IsCompact.elim_nhds_subcover' {X : Type u} [TopologicalSpace X] {s : Set X} (hs : IsCompact s) (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} [TopologicalSpace X] {s : Set X} (hs : IsCompact s) (U : XSet X) (hU : xs, U x nhds x) :
∃ (t : Finset X), (∀ xt, x s) s xt, 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 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} [TopologicalSpace X] {s : Set X} {l : Filter X} (hs : IsCompact s) :
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} [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 (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 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} [TopologicalSpace X] {s : Set X} {f : ιSet X} (hf : LocallyFinite f) (hs : IsCompact s) :
{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} [TopologicalSpace X] {s : Set X} {ι : Type v} (hs : IsCompact s) (t : ιSet X) (htc : ∀ (i : ι), IsClosed (t i)) (hst : ∀ (u : Finset ι), (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} [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.

@[deprecated IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed]
theorem IsCompact.nonempty_iInter_of_directed_nonempty_compact_closed {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

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

@[deprecated IsCompact.nonempty_iInter_of_sequence_nonempty_isCompact_isClosed]
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 : ), (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} [TopologicalSpace X] {s : Set X} {b : Set ι} {c : ιSet X} (hs : IsCompact s) (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} [TopologicalSpace X] {s : Set X} (h : ∀ {ι : Type u} (U : ιSet X), (∀ (i : ι), IsOpen (U i))s ⋃ (i : ι), U i∃ (t : Finset ι), 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} [TopologicalSpace X] {s : Set X} (h : ∀ {ι : Type u} (t : ιSet X), (∀ (i : ι), IsClosed (t i))s ⋂ (i : ι), t i = ∃ (u : Finset ι), 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} [TopologicalSpace X] {s : Set X} :
IsCompact s ∀ {ι : Type u} (U : ιSet X), (∀ (i : ι), IsOpen (U i))s ⋃ (i : ι), U i∃ (t : Finset ι), 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} [TopologicalSpace X] {s : Set X} :
IsCompact s ∀ {ι : Type u} (t : ιSet X), (∀ (i : ι), IsClosed (t i))s ⋂ (i : ι), t i = ∃ (u : Finset ι), 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} [TopologicalSpace X] {K : Set X} {Y : Type u_2} {l : Filter Y} {s : Set (X × Y)} (hK : IsCompact K) (hs : xK, s nhds x ×ˢ 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 = xK, 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 = yK, 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 : yK, s l ×ˢ nhds y) :

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 = xK, 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 = xK, 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 : xK, s nhds x 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 : yK, s l nhds y) :

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 : 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_singleton {X : Type u} [TopologicalSpace X] {x : X} :
theorem Set.Subsingleton.isCompact {X : Type u} [TopologicalSpace X] {s : Set X} (hs : s.Subsingleton) :
theorem Set.Finite.isCompact_biUnion {X : Type u} {ι : Type u_1} [TopologicalSpace X] {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} [TopologicalSpace X] (s : Finset ι) {f : ιSet X} (hf : is, IsCompact (f i)) :
IsCompact (⋃ is, f i)
theorem isCompact_accumulate {X : Type u} [TopologicalSpace X] {K : Set X} (hK : ∀ (n : ), IsCompact (K n)) (n : ) :
theorem Set.Finite.isCompact_sUnion {X : Type u} [TopologicalSpace X] {S : Set (Set X)} (hf : S.Finite) (hc : sS, 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 : s.Finite) :
theorem IsCompact.finite_of_discrete {X : Type u} [TopologicalSpace X] {s : Set X} [DiscreteTopology X] (hs : IsCompact s) :
s.Finite
theorem IsCompact.union {X : Type u} [TopologicalSpace X] {s : Set X} {t : Set X} (hs : IsCompact s) (ht : IsCompact t) :
theorem IsCompact.insert {X : Type u} [TopologicalSpace X] {s : Set X} (hs : IsCompact s) (a : X) :
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_nhd_of_compact for version assuming this.

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

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

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

@[deprecated]
theorem Nat.cocompact_eq :
Filter.cocompact = Filter.atTop
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)) :
theorem Filter.Tendsto.isCompact_insert_range {X : Type u} [TopologicalSpace X] {f : X} {x : X} (hf : Filter.Tendsto f Filter.atTop (nhds x)) :
theorem Filter.hasBasis_coclosedCompact {X : Type u} [TopologicalSpace X] :
(Filter.coclosedCompact X).HasBasis (fun (s : Set X) => IsClosed s IsCompact s) compl

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

@[deprecated Filter.mem_coclosedCompact_iff]
@[deprecated Filter.mem_coclosedCompact_iff]

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

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
Instances For
    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) :

    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} [TopologicalSpace X] {t : Set X} {f : Filter X} (ht : IsCompact t) (hf : Disjoint f (Filter.cocompact X)) :
    f ×ˢ nhdsSet t nhdsSet (Set.univ ×ˢ t)
    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.

    @[instance 10]
    Equations
    • =
    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
    @[deprecated exists_clusterPt_of_compactSpace]
    theorem cluster_point_of_compact {X : Type u} [TopologicalSpace X] [CompactSpace X] (f : Filter X) [f.NeBot] :
    ∃ (x : X), ClusterPt x f

    Alias of exists_clusterPt_of_compactSpace.

    theorem CompactSpace.elim_nhds_subcover {X : Type u} [TopologicalSpace X] [CompactSpace X] (U : XSet X) (hU : ∀ (x : X), U x nhds x) :
    ∃ (t : Finset X), xt, 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 ι), iu, t i = ) :
    theorem le_nhds_of_unique_clusterPt {X : Type u} [TopologicalSpace X] [CompactSpace X] {l : Filter X} {y : X} (h : ∀ (x : X), ClusterPt x lx = 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 : 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 IsCompact.ne_univ {X : Type u} [TopologicalSpace X] {s : Set X} [NoncompactSpace X] (hs : IsCompact s) :
    s Set.univ

    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 : s.Infinite) (hK : IsCompact K) (hsub : s K) :
    xK, 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 : s.Infinite) (hK : IsCompact K) (hsub : s K) :
    xK, 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 : XSet X} (hU : ∀ (x : X), U x nhds x) :
    ∃ (t : Finset X), xt, interior (U x) = Set.univ
    theorem finite_cover_nhds {X : Type u} [TopologicalSpace X] [CompactSpace X] {U : XSet X} (hU : ∀ (x : X), U x nhds x) :
    ∃ (t : Finset X), xt, 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) :
    {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} [TopologicalSpace X] [CompactSpace X] {f : ιSet X} (hf : LocallyFinite f) (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} [TopologicalSpace X] [CompactSpace X] {f : ιSet X} (hf : LocallyFinite f) (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
    Instances For

      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 : XY} (hf : Continuous f) :

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

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

      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 : XY} (hf : Embedding f) :

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

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

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

      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 : XProp} {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.finite {X : Type u} [TopologicalSpace X] {s : Set X} (hs : IsCompact s) (hs' : DiscreteTopology s) :
      s.Finite
      theorem exists_nhds_ne_inf_principal_neBot {X : Type u} [TopologicalSpace X] {s : Set X} (hs : IsCompact s) (hs' : s.Infinite) :
      zs, (nhdsWithin z {z} Filter.principal s).NeBot
      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) :
      @[instance 100]

      Finite topological spaces are compact.

      Equations
      • =

      The product of two compact spaces is compact.

      Equations
      • =

      The disjoint union of two compact spaces is compact.

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

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

      @[instance 100]
      Equations
      • =
      @[instance 100]
      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} [TopologicalSpace Y] [CompactSpace Y] :
      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 : 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 : ι) => 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 : XXProp} [CompactSpace X] :
      Equations
      • =
      Equations
      • =
      theorem IsClosed.exists_minimal_nonempty_closed_subset {X : Type u} [TopologicalSpace X] [CompactSpace X] {S : Set X} (hS : IsClosed S) (hne : S.Nonempty) :
      VS, V.Nonempty IsClosed V V'V, V'.NonemptyIsClosed V'V' = V