Mathlib.Topology.Compactness.Compact

IsCompact.exists_clusterPt theorem

(hs : IsCompact s) {f : Filter X} [NeBot f] (hf : f ≤ 𝓟 s) : ∃ x ∈ s, ClusterPt x f

Full source

lemma IsCompact.exists_clusterPt (hs : IsCompact s) {f : Filter X} [NeBot f] (hf : f ≤ 𝓟 s) :
    ∃ x ∈ s, ClusterPt x f := hs hf

Existence of Cluster Points in Compact Sets

Informal description

Let $X$ be a topological space and $s \subseteq X$ a compact subset. For any filter $f$ on $X$ that is not the trivial filter and satisfies $f \leq \mathcal{P}(s)$ (i.e., $f$ contains the principal filter of $s$), there exists a point $x \in s$ that is a cluster point of $f$.

IsCompact.exists_mapClusterPt theorem

 {ι : Type*} (hs : IsCompact s) {f : Filter ι} [NeBot f] {u : ι → X} (hf : Filter.map u f ≤ 𝓟 s) :
  ∃ x ∈ s, MapClusterPt x f u

Full source

lemma IsCompact.exists_mapClusterPt {ι : Type*} (hs : IsCompact s) {f : Filter ι} [NeBot f]
    {u : ι → X} (hf : Filter.map u f ≤ 𝓟 s) :
    ∃ x ∈ s, MapClusterPt x f u := hs hf

Existence of Cluster Points for Mapped Filters on Compact Sets

Informal description

Let $X$ be a topological space and $s \subseteq X$ a compact subset. For any type $\iota$, any non-trivial filter $f$ on $\iota$, and any function $u : \iota \to X$ such that the image filter $\text{map}\,u\,f$ is contained in the principal filter of $s$, there exists a point $x \in s$ that is a cluster point of $u$ with respect to $f$.

IsCompact.exists_clusterPt_of_frequently theorem

{l : Filter X} (hs : IsCompact s) (hl : ∃ᶠ x in l, x ∈ s) : ∃ a ∈ s, ClusterPt a l

Full source

lemma IsCompact.exists_clusterPt_of_frequently {l : Filter X} (hs : IsCompact s)
    (hl : ∃ᶠ x in l, x ∈ s) : ∃ a ∈ s, ClusterPt a l :=
  let ⟨a, has, ha⟩ := @hs _ (frequently_mem_iff_neBot.mp hl) inf_le_right
  ⟨a, has, ha.mono inf_le_left⟩

Existence of Cluster Points for Filters Frequently in Compact Sets

Informal description

Let $X$ be a topological space and $s \subseteq X$ a compact subset. For any filter $l$ on $X$ such that there exist infinitely many $x \in l$ with $x \in s$, there exists a point $a \in s$ that is a cluster point of $l$.

IsCompact.exists_mapClusterPt_of_frequently theorem

{l : Filter ι} {f : ι → X} (hs : IsCompact s) (hf : ∃ᶠ x in l, f x ∈ s) : ∃ a ∈ s, MapClusterPt a l f

Full source

lemma IsCompact.exists_mapClusterPt_of_frequently {l : Filter ι} {f : ι → X} (hs : IsCompact s)
    (hf : ∃ᶠ x in l, f x ∈ s) : ∃ a ∈ s, MapClusterPt a l f :=
  hs.exists_clusterPt_of_frequently hf

Existence of Cluster Points for Mapped Filters Frequently in Compact Sets

Informal description

Let $X$ be a topological space and $s \subseteq X$ a compact subset. For any filter $l$ on a type $\iota$ and any function $f : \iota \to X$ such that there exist infinitely many $x \in l$ with $f(x) \in s$, there exists a point $a \in s$ that is a cluster point of $f$ with respect to $l$.

IsCompact.compl_mem_sets theorem

(hs : IsCompact s) {f : Filter X} (hf : ∀ x ∈ s, sᶜ ∈ 𝓝 x ⊓ f) : sᶜ ∈ f

Full source

/-- 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 (hs : IsCompact s) {f : Filter X} (hf : ∀ x ∈ s, sᶜ ∈ 𝓝 x ⊓ f) :
    sᶜsᶜ ∈ f := by
  contrapose! hf
  simp only [not_mem_iff_inf_principal_compl, compl_compl, inf_assoc] at hf ⊢
  exact @hs _ hf inf_le_right

Complement of Compact Set Belongs to Filter if Locally Belongs

Informal description

Let $X$ be a topological space and $s \subseteq X$ a compact subset. For any filter $f$ on $X$, if the complement $s^c$ belongs to the neighborhood filter $\mathcal{N}_x \sqcap f$ for every $x \in s$, then $s^c$ belongs to $f$.

IsCompact.compl_mem_sets_of_nhdsWithin theorem

(hs : IsCompact s) {f : Filter X} (hf : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, tᶜ ∈ f) : sᶜ ∈ f

Full source

/-- 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.compl_mem_sets_of_nhdsWithin (hs : IsCompact s) {f : Filter X}
    (hf : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, tᶜ ∈ f) : sᶜsᶜ ∈ f := by
  refine hs.compl_mem_sets fun x hx => ?_
  rcases hf x hx with ⟨t, ht, hst⟩
  replace ht := mem_inf_principal.1 ht
  apply mem_inf_of_inter ht hst
  rintro x ⟨h₁, h₂⟩ hs
  exact h₂ (h₁ hs)

Complement of Compact Set Belongs to Filter if Locally Complement Belongs via Neighborhoods Within

Informal description

Let $X$ be a topological space and $s \subseteq X$ a compact subset. For any filter $f$ on $X$, if for every $x \in s$ there exists a neighborhood $t$ of $x$ within $s$ such that the complement $t^c$ belongs to $f$, then the complement $s^c$ belongs to $f$.

IsCompact.induction_on theorem

 (hs : IsCompact s) {p : Set X → Prop} (he : p ∅) (hmono : ∀ ⦃s t⦄, s ⊆ t → p t → p s)
  (hunion : ∀ ⦃s t⦄, p s → p t → p (s ∪ t)) (hnhds : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, p t) : p s

Full source

/-- 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. -/
@[elab_as_elim]
theorem IsCompact.induction_on (hs : IsCompact s) {p : Set X → Prop} (he : p ∅)
    (hmono : ∀ ⦃s t⦄, s ⊆ t → p t → p s) (hunion : ∀ ⦃s t⦄, p s → p t → p (s ∪ t))
    (hnhds : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, p t) : p s := by
  let f : Filter X := comk p he (fun _t ht _s hsub ↦ hmono hsub ht) (fun _s hs _t ht ↦ hunion hs ht)
  have : sᶜsᶜ ∈ f := hs.compl_mem_sets_of_nhdsWithin (by simpa [f] using hnhds)
  rwa [← compl_compl s]

Induction Principle for Compact Sets

Informal description

Let $X$ be a topological space and $s \subseteq X$ a compact subset. Suppose $p$ is a property of subsets of $X$ satisfying: 1. $p(\emptyset)$ holds, 2. $p$ is antitone (i.e., if $s \subseteq t$ and $p(t)$ holds, then $p(s)$ holds), 3. $p$ is stable under finite unions (i.e., if $p(s)$ and $p(t)$ hold, then $p(s \cup t)$ holds), and 4. For every $x \in s$, there exists a neighborhood $t$ of $x$ within $s$ such that $p(t)$ holds. Then $p(s)$ holds.

IsCompact.inter_right theorem

(hs : IsCompact s) (ht : IsClosed t) : IsCompact (s ∩ t)

Full source

/-- The intersection of a compact set and a closed set is a compact set. -/
theorem IsCompact.inter_right (hs : IsCompact s) (ht : IsClosed t) : IsCompact (s ∩ t) := by
  intro f hnf hstf
  obtain ⟨x, hsx, hx⟩ : ∃ x ∈ s, ClusterPt x f :=
    hs (le_trans hstf (le_principal_iff.2 inter_subset_left))
  have : x ∈ t := ht.mem_of_nhdsWithin_neBot <|
    hx.mono <| le_trans hstf (le_principal_iff.2 inter_subset_right)
  exact ⟨x, ⟨hsx, this⟩, hx⟩

Intersection of Compact and Closed Sets is Compact

Informal description

Let $s$ be a compact set and $t$ a closed set in a topological space $X$. Then the intersection $s \cap t$ is compact.

IsCompact.inter_left theorem

(ht : IsCompact t) (hs : IsClosed s) : IsCompact (s ∩ t)

Full source

/-- The intersection of a closed set and a compact set is a compact set. -/
theorem IsCompact.inter_left (ht : IsCompact t) (hs : IsClosed s) : IsCompact (s ∩ t) :=
  inter_comm t s ▸ ht.inter_right hs

Intersection of Closed and Compact Sets is Compact

Informal description

Let $t$ be a compact set and $s$ a closed set in a topological space $X$. Then the intersection $s \cap t$ is compact.

IsCompact.diff theorem

(hs : IsCompact s) (ht : IsOpen t) : IsCompact (s \ t)

Full source

/-- The set difference of a compact set and an open set is a compact set. -/
theorem IsCompact.diff (hs : IsCompact s) (ht : IsOpen t) : IsCompact (s \ t) :=
  hs.inter_right (isClosed_compl_iff.mpr ht)

Compactness of Set Difference with Open Set

Informal description

Let $s$ be a compact set and $t$ an open set in a topological space $X$. Then the set difference $s \setminus t$ is compact.

IsCompact.of_isClosed_subset theorem

(hs : IsCompact s) (ht : IsClosed t) (h : t ⊆ s) : IsCompact t

Full source

/-- A closed subset of a compact set is a compact set. -/
theorem IsCompact.of_isClosed_subset (hs : IsCompact s) (ht : IsClosed t) (h : t ⊆ s) :
    IsCompact t :=
  inter_eq_self_of_subset_right h ▸ hs.inter_right ht

Closed Subset of Compact Set is Compact

Informal description

Let $s$ be a compact set and $t$ a closed set in a topological space $X$. If $t$ is a subset of $s$, then $t$ is compact.

IsCompact.image_of_continuousOn theorem

{f : X → Y} (hs : IsCompact s) (hf : ContinuousOn f s) : IsCompact (f '' s)

Full source

theorem IsCompact.image_of_continuousOn {f : X → Y} (hs : IsCompact s) (hf : ContinuousOn f s) :
    IsCompact (f '' s) := by
  intro l lne ls
  have : NeBot (l.comap f ⊓ 𝓟 s) :=
    comap_inf_principal_neBot_of_image_mem lne (le_principal_iff.1 ls)
  obtain ⟨x, hxs, hx⟩ : ∃ x ∈ s, ClusterPt x (l.comap f ⊓ 𝓟 s) := @hs _ this inf_le_right
  haveI := hx.neBot
  use f x, mem_image_of_mem f hxs
  have : Tendsto f (𝓝𝓝 x ⊓ (comap f l ⊓ 𝓟 s)) (𝓝𝓝 (f x) ⊓ l) := by
    convert (hf x hxs).inf (@tendsto_comap _ _ f l) using 1
    rw [nhdsWithin]
    ac_rfl
  exact this.neBot

Continuous Image of Compact Set is Compact (restricted version)

Informal description

Let $X$ and $Y$ be topological spaces, $s \subseteq X$ a compact subset, and $f : X \to Y$ a function that is continuous on $s$. Then the image $f(s)$ is compact in $Y$.

IsCompact.image theorem

{f : X → Y} (hs : IsCompact s) (hf : Continuous f) : IsCompact (f '' s)

Full source

theorem IsCompact.image {f : X → Y} (hs : IsCompact s) (hf : Continuous f) : IsCompact (f '' s) :=
  hs.image_of_continuousOn hf.continuousOn

Continuous Image of Compact Set is Compact

Informal description

Let $X$ and $Y$ be topological spaces, $s \subseteq X$ a compact subset, and $f : X \to Y$ a continuous function. Then the image $f(s)$ is compact in $Y$.

IsCompact.adherence_nhdset theorem

 {f : Filter X} (hs : IsCompact s) (hf₂ : f ≤ 𝓟 s) (ht₁ : IsOpen t) (ht₂ : ∀ x ∈ s, ClusterPt x f → x ∈ t) : t ∈ f

Full source

theorem IsCompact.adherence_nhdset {f : Filter X} (hs : IsCompact s) (hf₂ : f ≤ 𝓟 s)
    (ht₁ : IsOpen t) (ht₂ : ∀ x ∈ s, ClusterPt x f → x ∈ t) : t ∈ f :=
  Classical.by_cases mem_of_eq_bot fun (this : f ⊓ 𝓟 tᶜf ⊓ 𝓟 tᶜ ≠ ⊥) =>
    let ⟨x, hx, (hfx : ClusterPt x <| f ⊓ 𝓟 tᶜ)⟩ := @hs _ ⟨this⟩ <| inf_le_of_left_le hf₂
    have : x ∈ t := ht₂ x hx hfx.of_inf_left
    have : tᶜtᶜ ∩ ttᶜ ∩ t ∈ 𝓝[tᶜ] x := inter_mem_nhdsWithin _ (IsOpen.mem_nhds ht₁ this)
    have A : 𝓝[tᶜ] x = ⊥ := empty_mem_iff_bot.1 <| compl_inter_self t ▸ this
    have : 𝓝[tᶜ] x𝓝[tᶜ] x ≠ ⊥ := hfx.of_inf_right.ne
    absurd A this

Compact Sets Adhere to Neighborhoods of Their Cluster Points

Informal description

Let $X$ be a topological space and $s \subseteq X$ be a compact subset. For any filter $f$ on $X$ such that $f$ is finer than the principal filter generated by $s$, and for any open set $t \subseteq X$ containing all points $x \in s$ that are cluster points of $f$, we have $t \in f$.

isCompact_iff_ultrafilter_le_nhds theorem

: IsCompact s ↔ ∀ f : Ultrafilter X, ↑f ≤ 𝓟 s → ∃ x ∈ s, ↑f ≤ 𝓝 x

Full source

theorem isCompact_iff_ultrafilter_le_nhds :
    IsCompactIsCompact s ↔ ∀ f : Ultrafilter X, ↑f ≤ 𝓟 s → ∃ x ∈ s, ↑f ≤ 𝓝 x := by
  refine (forall_neBot_le_iff ?_).trans ?_
  · rintro f g hle ⟨x, hxs, hxf⟩
    exact ⟨x, hxs, hxf.mono hle⟩
  · simp only [Ultrafilter.clusterPt_iff]

Characterization of Compactness via Ultrafilter Convergence

Informal description

A subset $s$ of a topological space $X$ is compact if and only if for every ultrafilter $f$ on $X$ such that $f$ contains $s$, there exists a point $x \in s$ such that $f$ converges to $x$.

isCompact_iff_ultrafilter_le_nhds' theorem

: IsCompact s ↔ ∀ f : Ultrafilter X, s ∈ f → ∃ x ∈ s, ↑f ≤ 𝓝 x

Full source

theorem isCompact_iff_ultrafilter_le_nhds' :
    IsCompactIsCompact s ↔ ∀ f : Ultrafilter X, s ∈ f → ∃ x ∈ s, ↑f ≤ 𝓝 x := by
  simp only [isCompact_iff_ultrafilter_le_nhds, le_principal_iff, Ultrafilter.mem_coe]

Ultrafilter Characterization of Compactness

Informal description

A subset $s$ of a topological space $X$ is compact if and only if for every ultrafilter $f$ on $X$ that contains $s$, there exists a point $x \in s$ such that $f$ converges to $x$.

IsCompact.le_nhds_of_unique_clusterPt theorem

(hs : IsCompact s) {l : Filter X} {y : X} (hmem : s ∈ l) (h : ∀ x ∈ s, ClusterPt x l → x = y) : l ≤ 𝓝 y

Full source

/-- 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`. -/
lemma IsCompact.le_nhds_of_unique_clusterPt (hs : IsCompact s) {l : Filter X} {y : X}
    (hmem : s ∈ l) (h : ∀ x ∈ s, ClusterPt x l → x = y) : l ≤ 𝓝 y := by
  refine le_iff_ultrafilter.2 fun f hf ↦ ?_
  rcases hs.ultrafilter_le_nhds' f (hf hmem) with ⟨x, hxs, hx⟩
  convert ← hx
  exact h x hxs (.mono (.of_le_nhds hx) hf)

Convergence of Filter with Unique Cluster Point in Compact Set

Informal description

Let $s$ be a compact subset of a topological space $X$, and let $l$ be a filter on $X$ such that $s \in l$. If $y \in X$ is the unique cluster point of $l$ in $s$ (i.e., for all $x \in s$, if $x$ is a cluster point of $l$ then $x = y$), then $l$ converges to $y$.

IsCompact.tendsto_nhds_of_unique_mapClusterPt theorem

 {Y} {l : Filter Y} {y : X} {f : Y → X} (hs : IsCompact s) (hmem : ∀ᶠ x in l, f x ∈ s)
  (h : ∀ x ∈ s, MapClusterPt x l f → x = y) : Tendsto f l (𝓝 y)

Full source

/-- 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`. -/
lemma IsCompact.tendsto_nhds_of_unique_mapClusterPt {Y} {l : Filter Y} {y : X} {f : Y → X}
    (hs : IsCompact s) (hmem : ∀ᶠ x in l, f x ∈ s) (h : ∀ x ∈ s, MapClusterPt x l f → x = y) :
    Tendsto f l (𝓝 y) :=
  hs.le_nhds_of_unique_clusterPt (mem_map.2 hmem) h

Convergence of Function with Unique Cluster Point in Compact Set

Informal description

Let $s$ be a compact subset of a topological space $X$, and let $f : Y \to X$ be a function. Suppose that for any filter $l$ on $Y$, the values of $f$ eventually lie in $s$ along $l$. If $y \in X$ is the unique point in $s$ such that $y$ is a cluster point of $f$ along $l$ (i.e., for all $x \in s$, if $x$ is a cluster point of $f$ along $l$ then $x = y$), then $f$ tends to $y$ along $l$.

IsCompact.elim_directed_cover theorem

 {ι : Type v} [hι : Nonempty ι] (hs : IsCompact s) (U : ι → Set X) (hUo : ∀ i, IsOpen (U i)) (hsU : s ⊆ ⋃ i, U i)
  (hdU : Directed (· ⊆ ·) U) : ∃ i, s ⊆ U i

Full source

/-- 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_directed_cover {ι : Type v} [hι : Nonempty ι] (hs : IsCompact s)
    (U : ι → Set X) (hUo : ∀ i, IsOpen (U i)) (hsU : s ⊆ ⋃ i, U i) (hdU : Directed (· ⊆ ·) U) :
    ∃ i, s ⊆ U i :=
  hι.elim fun i₀ =>
    IsCompact.induction_on hs ⟨i₀, empty_subset _⟩ (fun _ _ hs ⟨i, hi⟩ => ⟨i, hs.trans hi⟩)
      (fun _ _ ⟨i, hi⟩ ⟨j, hj⟩ =>
        let ⟨k, hki, hkj⟩ := hdU i j
        ⟨k, union_subset (Subset.trans hi hki) (Subset.trans hj hkj)⟩)
      fun _x hx =>
      let ⟨i, hi⟩ := mem_iUnion.1 (hsU hx)
      ⟨U i, mem_nhdsWithin_of_mem_nhds (IsOpen.mem_nhds (hUo i) hi), i, Subset.refl _⟩

Compact Set Covered by Directed Open Family Has Single Covering Element

Informal description

Let $X$ be a topological space and $s \subseteq X$ a compact subset. Given a nonempty directed family of open sets $\{U_i\}_{i \in \iota}$ in $X$ such that $s \subseteq \bigcup_{i \in \iota} U_i$, there exists an index $i \in \iota$ such that $s \subseteq U_i$.

IsCompact.elim_finite_subcover theorem

 {ι : 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

Full source

/-- For every open cover of a compact set, there exists a finite subcover. -/
theorem IsCompact.elim_finite_subcover {ι : 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 :=
  hs.elim_directed_cover _ (fun _ => isOpen_biUnion fun i _ => hUo i)
    (iUnion_eq_iUnion_finset U ▸ hsU)
    (directed_of_isDirected_le fun _ _ h => biUnion_subset_biUnion_left h)

Finite Subcover Property of Compact Sets

Informal description

Let $X$ be a topological space and $s \subseteq X$ a compact subset. For any open cover $\{U_i\}_{i \in \iota}$ of $s$ (i.e., $s \subseteq \bigcup_{i \in \iota} U_i$ with each $U_i$ open), there exists a finite subset $t \subseteq \iota$ such that $s \subseteq \bigcup_{i \in t} U_i$.

IsCompact.elim_nhds_subcover_nhdsSet' theorem

 (hs : IsCompact s) (U : ∀ x ∈ s, Set X) (hU : ∀ x hx, U x hx ∈ 𝓝 x) : ∃ t : Finset s, (⋃ x ∈ t, U x.1 x.2) ∈ 𝓝ˢ s

Full source

lemma IsCompact.elim_nhds_subcover_nhdsSet' (hs : IsCompact s) (U : ∀ x ∈ s, Set X)
    (hU : ∀ x hx, U x hx ∈ 𝓝 x) : ∃ t : Finset s, (⋃ x ∈ t, U x.1 x.2) ∈ 𝓝ˢ s := by
  rcases hs.elim_finite_subcover (fun x : s ↦ interior (U x x.2)) (fun _ ↦ isOpen_interior)
    fun x hx ↦ mem_iUnion.2 ⟨⟨x, hx⟩, mem_interior_iff_mem_nhds.2 <| hU _ _⟩ with ⟨t, hst⟩
  refine ⟨t, mem_nhdsSet_iff_forall.2 fun x hx ↦ ?_⟩
  rcases mem_iUnion₂.1 (hst hx) with ⟨y, hyt, hy⟩
  refine mem_of_superset ?_ (subset_biUnion_of_mem hyt)
  exact mem_interior_iff_mem_nhds.1 hy

Finite Neighborhood Subcover Property for Compact Sets

Informal description

Let $X$ be a topological space and $s \subseteq X$ a compact subset. Given for each $x \in s$ a neighborhood $U_x$ of $x$ (i.e., $U_x \in \mathcal{N}(x)$), there exists a finite subset $t \subseteq s$ such that the union $\bigcup_{x \in t} U_x$ is a neighborhood of $s$ (i.e., $\bigcup_{x \in t} U_x \in \mathcal{N}^s(s)$).

IsCompact.elim_nhds_subcover_nhdsSet theorem

 (hs : IsCompact s) {U : X → Set X} (hU : ∀ x ∈ s, U x ∈ 𝓝 x) : ∃ t : Finset X, (∀ x ∈ t, x ∈ s) ∧ (⋃ x ∈ t, U x) ∈ 𝓝ˢ s

Full source

lemma IsCompact.elim_nhds_subcover_nhdsSet (hs : IsCompact s) {U : X → Set X}
    (hU : ∀ x ∈ s, U x ∈ 𝓝 x) : ∃ t : Finset X, (∀ x ∈ t, x ∈ s) ∧ (⋃ x ∈ t, U x) ∈ 𝓝ˢ s := by
  let ⟨t, ht⟩ := hs.elim_nhds_subcover_nhdsSet' (fun x _ => U x) hU
  classical
  exact ⟨t.image (↑), fun x hx =>
    let ⟨y, _, hyx⟩ := Finset.mem_image.1 hx
    hyx ▸ y.2,
    by rwa [Finset.set_biUnion_finset_image]⟩

Finite Neighborhood Subcover Property for Compact Sets (Pointwise Version)

Informal description

Let $X$ be a topological space and $s \subseteq X$ a compact subset. Given a family of neighborhoods $\{U_x\}_{x \in s}$ (i.e., $U_x \in \mathcal{N}(x)$ for each $x \in s$), there exists a finite subset $t \subseteq s$ such that the union $\bigcup_{x \in t} U_x$ is a neighborhood of $s$ (i.e., $\bigcup_{x \in t} U_x \in \mathcal{N}^s(s)$).

IsCompact.elim_nhds_subcover' theorem

 (hs : IsCompact s) (U : ∀ x ∈ s, Set X) (hU : ∀ x (hx : x ∈ s), U x ‹x ∈ s› ∈ 𝓝 x) :
  ∃ t : Finset s, s ⊆ ⋃ x ∈ t, U (x : s) x.2

Full source

theorem IsCompact.elim_nhds_subcover' (hs : IsCompact s) (U : ∀ x ∈ s, Set X)
    (hU : ∀ x (hx : x ∈ s), U x ‹x ∈ s› ∈ 𝓝 x) : ∃ t : Finset s, s ⊆ ⋃ x ∈ t, U (x : s) x.2 :=
  (hs.elim_nhds_subcover_nhdsSet' U hU).imp fun _ ↦ subset_of_mem_nhdsSet

Finite Subcover Property for Compact Sets

Informal description

Let $X$ be a topological space and $s \subseteq X$ a compact subset. Given for each $x \in s$ a neighborhood $U_x$ of $x$ (i.e., $U_x \in \mathcal{N}(x)$), there exists a finite subset $t \subseteq s$ such that $s$ is covered by the union $\bigcup_{x \in t} U_x$.

IsCompact.elim_nhds_subcover theorem

 (hs : IsCompact s) (U : X → Set X) (hU : ∀ x ∈ s, U x ∈ 𝓝 x) : ∃ t : Finset X, (∀ x ∈ t, x ∈ s) ∧ s ⊆ ⋃ x ∈ t, U x

Full source

theorem IsCompact.elim_nhds_subcover (hs : IsCompact s) (U : X → Set X) (hU : ∀ x ∈ s, U x ∈ 𝓝 x) :
    ∃ t : Finset X, (∀ x ∈ t, x ∈ s) ∧ s ⊆ ⋃ x ∈ t, U x :=
  (hs.elim_nhds_subcover_nhdsSet hU).imp fun _ h ↦ h.imp_right subset_of_mem_nhdsSet

Finite Subcover Property for Compact Sets

Informal description

Let $X$ be a topological space and $s \subseteq X$ a compact subset. Given a family of neighborhoods $\{U_x\}_{x \in X}$ such that $U_x$ is a neighborhood of $x$ for each $x \in s$, there exists a finite subset $t \subseteq s$ such that $s$ is covered by the union $\bigcup_{x \in t} U_x$.

IsCompact.elim_nhdsWithin_subcover' theorem

 (hs : IsCompact s) (U : ∀ x ∈ s, Set X) (hU : ∀ x (hx : x ∈ s), U x hx ∈ 𝓝[s] x) : ∃ t : Finset s, s ⊆ ⋃ x ∈ t, U x x.2

Full source

theorem IsCompact.elim_nhdsWithin_subcover' (hs : IsCompact s) (U : ∀ x ∈ s, Set X)
    (hU : ∀ x (hx : x ∈ s), U x hx ∈ 𝓝[s] x) : ∃ t : Finset s, s ⊆ ⋃ x ∈ t, U x x.2 := by
  choose V V_nhds hV using fun x hx => mem_nhdsWithin_iff_exists_mem_nhds_inter.1 (hU x hx)
  refine (hs.elim_nhds_subcover' V V_nhds).imp fun t ht =>
    subset_trans ?_ (iUnion₂_mono fun x _ => hV x x.2)
  simpa [← iUnion_inter, ← iUnion_coe_set]

Finite Relative Subcover Property for Compact Sets

Informal description

Let $X$ be a topological space and $s \subseteq X$ a compact subset. Given for each $x \in s$ a neighborhood $U_x$ of $x$ relative to $s$ (i.e., $U_x \in \mathcal{N}_s(x)$), there exists a finite subset $t \subseteq s$ such that $s$ is covered by the union $\bigcup_{x \in t} U_x$.

IsCompact.elim_nhdsWithin_subcover theorem

 (hs : IsCompact s) (U : X → Set X) (hU : ∀ x ∈ s, U x ∈ 𝓝[s] x) : ∃ t : Finset X, (∀ x ∈ t, x ∈ s) ∧ s ⊆ ⋃ x ∈ t, U x

Full source

theorem IsCompact.elim_nhdsWithin_subcover (hs : IsCompact s) (U : X → Set X)
    (hU : ∀ x ∈ s, U x ∈ 𝓝[s] x) : ∃ t : Finset X, (∀ x ∈ t, x ∈ s) ∧ s ⊆ ⋃ x ∈ t, U x := by
  choose! V V_nhds hV using fun x hx => mem_nhdsWithin_iff_exists_mem_nhds_inter.1 (hU x hx)
  refine (hs.elim_nhds_subcover V V_nhds).imp fun t ⟨t_sub_s, ht⟩ =>
    ⟨t_sub_s, subset_trans ?_ (iUnion₂_mono fun x hx => hV x (t_sub_s x hx))⟩
  simpa [← iUnion_inter]

Finite Relative Subcover Property for Compact Sets

Informal description

Let $X$ be a topological space and $s \subseteq X$ a compact subset. Given a family of sets $\{U_x\}_{x \in X}$ such that for each $x \in s$, $U_x$ is a neighborhood of $x$ relative to $s$ (i.e., $U_x \in \mathcal{N}_s(x)$), there exists a finite subset $t \subseteq s$ such that $s$ is covered by the union $\bigcup_{x \in t} U_x$.

IsCompact.disjoint_nhdsSet_left theorem

{l : Filter X} (hs : IsCompact s) : Disjoint (𝓝ˢ s) l ↔ ∀ x ∈ s, Disjoint (𝓝 x) l

Full source

/-- 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_left {l : Filter X} (hs : IsCompact s) :
    DisjointDisjoint (𝓝ˢ s) l ↔ ∀ x ∈ s, Disjoint (𝓝 x) l := by
  refine ⟨fun h x hx => h.mono_left <| nhds_le_nhdsSet hx, fun H => ?_⟩
  choose! U hxU hUl using fun x hx => (nhds_basis_opens x).disjoint_iff_left.1 (H x hx)
  choose hxU hUo using hxU
  rcases hs.elim_nhds_subcover U fun x hx => (hUo x hx).mem_nhds (hxU x hx) with ⟨t, hts, hst⟩
  refine (hasBasis_nhdsSet _).disjoint_iff_left.2
    ⟨⋃ x ∈ t, U x, ⟨isOpen_biUnion fun x hx => hUo x (hts x hx), hst⟩, ?_⟩
  rw [compl_iUnion₂, biInter_finset_mem]
  exact fun x hx => hUl x (hts x hx)

Disjointness of Neighborhood Filter of Compact Set vs Pointwise Neighborhood Filters

Informal description

Let $X$ be a topological space and $s \subseteq X$ a compact subset. For any filter $l$ on $X$, the neighborhood filter of $s$ is disjoint with $l$ if and only if for every point $x \in s$, the neighborhood filter of $x$ is disjoint with $l$.

IsCompact.disjoint_nhdsSet_right theorem

{l : Filter X} (hs : IsCompact s) : Disjoint l (𝓝ˢ s) ↔ ∀ x ∈ s, Disjoint l (𝓝 x)

Full source

/-- 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.disjoint_nhdsSet_right {l : Filter X} (hs : IsCompact s) :
    DisjointDisjoint l (𝓝ˢ s) ↔ ∀ x ∈ s, Disjoint l (𝓝 x) := by
  simpa only [disjoint_comm] using hs.disjoint_nhdsSet_left

Disjointness of Filter with Neighborhood Filter of Compact Set vs Pointwise Neighborhood Filters

Informal description

Let $X$ be a topological space and $s \subseteq X$ a compact subset. For any filter $l$ on $X$, $l$ is disjoint with the neighborhood filter of $s$ if and only if for every point $x \in s$, $l$ is disjoint with the neighborhood filter of $x$.

IsCompact.elim_directed_family_closed theorem

 {ι : Type v} [Nonempty ι] (hs : IsCompact s) (t : ι → Set X) (htc : ∀ i, IsClosed (t i)) (hst : (s ∩ ⋂ i, t i) = ∅)
  (hdt : Directed (· ⊇ ·) t) : ∃ i : ι, s ∩ t i = ∅

Full source

/-- 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_directed_family_closed {ι : Type v} [Nonempty ι] (hs : IsCompact s)
    (t : ι → Set X) (htc : ∀ i, IsClosed (t i)) (hst : (s ∩ ⋂ i, t i) = ∅)
    (hdt : Directed (· ⊇ ·) t) : ∃ i : ι, s ∩ t i = ∅ :=
  let ⟨t, ht⟩ :=
    hs.elim_directed_cover (complcompl ∘ t) (fun i => (htc i).isOpen_compl)
      (by
        simpa only [subset_def, not_forall, eq_empty_iff_forall_not_mem, mem_iUnion, exists_prop,
          mem_inter_iff, not_and, mem_iInter, mem_compl_iff] using hst)
      (hdt.mono_comp _ fun _ _ => compl_subset_compl.mpr)
  ⟨t, by
    simpa only [subset_def, not_forall, eq_empty_iff_forall_not_mem, mem_iUnion, exists_prop,
      mem_inter_iff, not_and, mem_iInter, mem_compl_iff] using ht⟩

Compact Set Avoids Directed Intersection of Closed Sets

Informal description

Let $X$ be a topological space and $s \subseteq X$ a compact subset. Given a nonempty directed family of closed sets $\{t_i\}_{i \in \iota}$ in $X$ such that $s \cap \bigcap_{i \in \iota} t_i = \emptyset$ and the family is directed with respect to reverse inclusion ($\supseteq$), there exists an index $i \in \iota$ such that $s \cap t_i = \emptyset$.

IsCompact.elim_finite_subfamily_closed theorem

 {ι : 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) = ∅

Full source

/-- For every family of closed sets whose intersection avoids a compact set,
there exists a finite subfamily whose intersection avoids this compact set. -/
theorem IsCompact.elim_finite_subfamily_closed {ι : 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) = ∅ :=
  hs.elim_directed_family_closed _ (fun _ ↦ isClosed_biInter fun _ _ ↦ htc _)
    (by rwa [← iInter_eq_iInter_finset])
    (directed_of_isDirected_le fun _ _ h ↦ biInter_subset_biInter_left h)

Finite Subfamily Property for Compact Sets and Closed Sets

Informal description

Let $X$ be a topological space and $s \subseteq X$ a compact subset. Given a family of closed sets $\{t_i\}_{i \in \iota}$ in $X$ such that $s \cap \bigcap_{i \in \iota} t_i = \emptyset$, there exists a finite subset $u \subseteq \iota$ such that $s \cap \bigcap_{i \in u} t_i = \emptyset$.

IsCompact.inter_iInter_nonempty theorem

 {ι : Type v} (hs : IsCompact s) (t : ι → Set X) (htc : ∀ i, IsClosed (t i))
  (hst : ∀ u : Finset ι, (s ∩ ⋂ i ∈ u, t i).Nonempty) : (s ∩ ⋂ i, t i).Nonempty

Full source

/-- 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.inter_iInter_nonempty {ι : Type v} (hs : IsCompact s) (t : ι → Set X)
    (htc : ∀ i, IsClosed (t i)) (hst : ∀ u : Finset ι, (s ∩ ⋂ i ∈ u, t i).Nonempty) :
    (s ∩ ⋂ i, t i).Nonempty := by
  contrapose! hst
  exact hs.elim_finite_subfamily_closed t htc hst

Compact Set Intersection Property for Families of Closed Sets

Informal description

Let $X$ be a topological space, $s \subseteq X$ a compact subset, and $\{t_i\}_{i \in \iota}$ a family of closed subsets of $X$. If for every finite subset $u \subseteq \iota$, the intersection $s \cap \bigcap_{i \in u} t_i$ is nonempty, then the intersection $s \cap \bigcap_{i \in \iota} t_i$ is also nonempty.

IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed theorem

 {ι : Type v} [hι : Nonempty ι] (t : ι → Set X) (htd : Directed (· ⊇ ·) t) (htn : ∀ i, (t i).Nonempty)
  (htc : ∀ i, IsCompact (t i)) (htcl : ∀ i, IsClosed (t i)) : (⋂ i, t i).Nonempty

Full source

/-- Cantor's intersection theorem for `iInter`:
the intersection of a directed family of nonempty compact closed sets is nonempty. -/
theorem IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed
    {ι : Type v} [hι : Nonempty ι] (t : ι → Set X) (htd : Directed (· ⊇ ·) t)
    (htn : ∀ i, (t i).Nonempty) (htc : ∀ i, IsCompact (t i)) (htcl : ∀ i, IsClosed (t i)) :
    (⋂ i, t i).Nonempty := by
  let i₀ := hι.some
  suffices (t i₀ ∩ ⋂ i, t i).Nonempty by
    rwa [inter_eq_right.mpr (iInter_subset _ i₀)] at this
  simp only [nonempty_iff_ne_empty] at htn ⊢
  apply mt ((htc i₀).elim_directed_family_closed t htcl)
  push_neg
  simp only [← nonempty_iff_ne_empty] at htn ⊢
  refine ⟨htd, fun i => ?_⟩
  rcases htd i₀ i with ⟨j, hji₀, hji⟩
  exact (htn j).mono (subset_inter hji₀ hji)

Cantor's Intersection Theorem for Directed Families of Compact Closed Sets

Informal description

Let $X$ be a topological space and $\{t_i\}_{i \in \iota}$ a nonempty directed family of nonempty compact closed subsets of $X$ with respect to reverse inclusion ($\supseteq$). Then the intersection $\bigcap_{i \in \iota} t_i$ is nonempty.

IsCompact.nonempty_sInter_of_directed_nonempty_isCompact_isClosed theorem

 {S : Set (Set X)} [hS : Nonempty S] (hSd : DirectedOn (· ⊇ ·) S) (hSn : ∀ U ∈ S, U.Nonempty)
  (hSc : ∀ U ∈ S, IsCompact U) (hScl : ∀ U ∈ S, IsClosed U) : (⋂₀ S).Nonempty

Full source

/-- Cantor's intersection theorem for `sInter`:
the intersection of a directed family of nonempty compact closed sets is nonempty. -/
theorem IsCompact.nonempty_sInter_of_directed_nonempty_isCompact_isClosed
    {S : Set (Set X)} [hS : Nonempty S] (hSd : DirectedOn (· ⊇ ·) S) (hSn : ∀ U ∈ S, U.Nonempty)
    (hSc : ∀ U ∈ S, IsCompact U) (hScl : ∀ U ∈ S, IsClosed U) : (⋂₀ S).Nonempty := by
  rw [sInter_eq_iInter]
  exact IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed _
    (DirectedOn.directed_val hSd) (fun i ↦ hSn i i.2) (fun i ↦ hSc i i.2) (fun i ↦ hScl i i.2)

Cantor's Intersection Theorem for Directed Collections of Compact Closed Sets

Informal description

Let $X$ be a topological space and $S$ a nonempty collection of nonempty compact closed subsets of $X$ that is directed with respect to reverse inclusion ($\supseteq$). Then the intersection $\bigcap_{U \in S} U$ is nonempty.

IsCompact.nonempty_iInter_of_sequence_nonempty_isCompact_isClosed theorem

 (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

Full source

/-- Cantor's intersection theorem for sequences indexed by `ℕ`:
the intersection of a decreasing sequence of nonempty compact closed sets is nonempty. -/
theorem IsCompact.nonempty_iInter_of_sequence_nonempty_isCompact_isClosed (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 :=
  have tmono : Antitone t := antitone_nat_of_succ_le htd
  have htd : Directed (· ⊇ ·) t := tmono.directed_ge
  have : ∀ i, t i ⊆ t 0 := fun i => tmono <| Nat.zero_le i
  have htc : ∀ i, IsCompact (t i) := fun i => ht0.of_isClosed_subset (htcl i) (this i)
  IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed t htd htn htc htcl

Cantor's Intersection Theorem for Sequences of Compact Closed Sets

Informal description

Let $X$ be a topological space and $(t_n)_{n \in \mathbb{N}}$ a decreasing sequence of nonempty compact closed subsets of $X$ (i.e., $t_{n+1} \subseteq t_n$ for all $n \in \mathbb{N}$). Then the intersection $\bigcap_{n \in \mathbb{N}} t_n$ is nonempty.

IsCompact.elim_finite_subcover_image theorem

 {b : Set ι} {c : ι → Set X} (hs : IsCompact s) (hc₁ : ∀ i ∈ b, IsOpen (c i)) (hc₂ : s ⊆ ⋃ i ∈ b, c i) :
  ∃ b', b' ⊆ b ∧ Set.Finite b' ∧ s ⊆ ⋃ i ∈ b', c i

Full source

/-- For every open cover of a compact set, there exists a finite subcover. -/
theorem IsCompact.elim_finite_subcover_image {b : Set ι} {c : ι → Set X} (hs : IsCompact s)
    (hc₁ : ∀ i ∈ b, IsOpen (c i)) (hc₂ : s ⊆ ⋃ i ∈ b, c i) :
    ∃ b', b' ⊆ b ∧ Set.Finite b' ∧ s ⊆ ⋃ i ∈ b', c i := by
  simp only [Subtype.forall', biUnion_eq_iUnion] at hc₁ hc₂
  rcases hs.elim_finite_subcover (fun i => c i : b → Set X) hc₁ hc₂ with ⟨d, hd⟩
  refine ⟨Subtype.val '' d.toSet, ?_, d.finite_toSet.image _, ?_⟩
  · simp
  · rwa [biUnion_image]

Finite Subcover Property of Compact Sets for Indexed Families

Informal description

Let $X$ be a topological space and $s \subseteq X$ a compact subset. Given a family of open sets $\{c_i\}_{i \in b}$ indexed by a set $b$ such that $s \subseteq \bigcup_{i \in b} c_i$, there exists a finite subset $b' \subseteq b$ such that $s \subseteq \bigcup_{i \in b'} c_i$.

isCompact_of_finite_subcover theorem

 (h : ∀ {ι : Type u} (U : ι → Set X), (∀ i, IsOpen (U i)) → (s ⊆ ⋃ i, U i) → ∃ t : Finset ι, s ⊆ ⋃ i ∈ t, U i) :
  IsCompact s

Full source

/-- A set `s` is compact if for every open cover of `s`, there exists a finite subcover. -/
theorem isCompact_of_finite_subcover
    (h : ∀ {ι : Type u} (U : ι → Set X), (∀ i, IsOpen (U i)) → (s ⊆ ⋃ i, U i) →
      ∃ t : Finset ι, s ⊆ ⋃ i ∈ t, U i) :
    IsCompact s := fun f hf hfs => by
  contrapose! h
  simp only [ClusterPt, not_neBot, ← disjoint_iff, SetCoe.forall',
    (nhds_basis_opens _).disjoint_iff_left] at h
  choose U hU hUf using h
  refine ⟨s, U, fun x => (hU x).2, fun x hx => mem_iUnion.2 ⟨⟨x, hx⟩, (hU _).1⟩, fun t ht => ?_⟩
  refine compl_not_mem (le_principal_iff.1 hfs) ?_
  refine mem_of_superset ((biInter_finset_mem t).2 fun x _ => hUf x) ?_
  rw [subset_compl_comm, compl_iInter₂]
  simpa only [compl_compl]

Compactness via Finite Subcovers

Informal description

A subset $s$ of a topological space $X$ is compact if for every family of open sets $(U_i)_{i \in \iota}$ covering $s$ (i.e., $s \subseteq \bigcup_{i \in \iota} U_i$), there exists a finite subset of indices $t \subseteq \iota$ such that $s$ is still covered by the corresponding finite subfamily $(U_i)_{i \in t}$ (i.e., $s \subseteq \bigcup_{i \in t} U_i$).

isCompact_of_finite_subfamily_closed theorem


  (h :
    ∀ {ι : Type u} (t : ι → Set X),
      (∀ i, IsClosed (t i)) → (s ∩ ⋂ i, t i) = ∅ → ∃ u : Finset ι, (s ∩ ⋂ i ∈ u, t i) = ∅) :
  IsCompact s

Full source

/-- 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_of_finite_subfamily_closed
    (h : ∀ {ι : Type u} (t : ι → Set X), (∀ i, IsClosed (t i)) → (s ∩ ⋂ i, t i) = ∅ →
      ∃ u : Finset ι, (s ∩ ⋂ i ∈ u, t i) = ∅) :
    IsCompact s :=
  isCompact_of_finite_subcover fun U hUo hsU => by
    rw [← disjoint_compl_right_iff_subset, compl_iUnion, disjoint_iff] at hsU
    rcases h (fun i => (U i)ᶜ) (fun i => (hUo _).isClosed_compl) hsU with ⟨t, ht⟩
    refine ⟨t, ?_⟩
    rwa [← disjoint_compl_right_iff_subset, compl_iUnion₂, disjoint_iff]

Compactness via Finite Subfamily of Closed Sets

Informal description

A subset $s$ of a topological space $X$ is compact if for every family of closed sets $(t_i)_{i \in \iota}$ such that the intersection of $s$ with the intersection of all $t_i$ is empty (i.e., $s \cap \bigcap_{i \in \iota} t_i = \emptyset$), there exists a finite subset of indices $u \subseteq \iota$ such that the intersection of $s$ with the intersection of the corresponding finite subfamily $(t_i)_{i \in u}$ is still empty (i.e., $s \cap \bigcap_{i \in u} t_i = \emptyset$).

isCompact_iff_finite_subcover theorem

 : IsCompact s ↔ ∀ {ι : Type u} (U : ι → Set X), (∀ i, IsOpen (U i)) → (s ⊆ ⋃ i, U i) → ∃ t : Finset ι, s ⊆ ⋃ i ∈ t, U i

Full source

/-- A set `s` is compact if and only if
for every open cover of `s`, there exists a finite subcover. -/
theorem isCompact_iff_finite_subcover :
    IsCompactIsCompact s ↔ ∀ {ι : Type u} (U : ι → Set X),
      (∀ i, IsOpen (U i)) → (s ⊆ ⋃ i, U i) → ∃ t : Finset ι, s ⊆ ⋃ i ∈ t, U i :=
  ⟨fun hs => hs.elim_finite_subcover, isCompact_of_finite_subcover⟩

Compactness via Finite Open Covers

Informal description

A subset $s$ of a topological space $X$ is compact if and only if for every family of open sets $\{U_i\}_{i \in \iota}$ covering $s$ (i.e., $s \subseteq \bigcup_{i \in \iota} U_i$), there exists a finite subset of indices $t \subseteq \iota$ such that $s \subseteq \bigcup_{i \in t} U_i$.

isCompact_iff_finite_subfamily_closed theorem

 :
  IsCompact s ↔
    ∀ {ι : Type u} (t : ι → Set X), (∀ i, IsClosed (t i)) → (s ∩ ⋂ i, t i) = ∅ → ∃ u : Finset ι, (s ∩ ⋂ i ∈ u, t i) = ∅

Full source

/-- 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_iff_finite_subfamily_closed :
    IsCompactIsCompact s ↔ ∀ {ι : Type u} (t : ι → Set X),
      (∀ i, IsClosed (t i)) → (s ∩ ⋂ i, t i) = ∅ → ∃ u : Finset ι, (s ∩ ⋂ i ∈ u, t i) = ∅ :=
  ⟨fun hs => hs.elim_finite_subfamily_closed, isCompact_of_finite_subfamily_closed⟩

Compactness Criterion via Finite Intersection Property for Closed Sets

Informal description

A subset $s$ of a topological space $X$ is compact if and only if for every family of closed sets $\{t_i\}_{i \in \iota}$ in $X$ such that $s \cap \bigcap_{i \in \iota} t_i = \emptyset$, there exists a finite subset $u \subseteq \iota$ such that $s \cap \bigcap_{i \in u} t_i = \emptyset$.

IsCompact.mem_nhdsSet_prod_of_forall theorem

 {K : Set X} {Y} {l : Filter Y} {s : Set (X × Y)} (hK : IsCompact K) (hs : ∀ x ∈ K, s ∈ 𝓝 x ×ˢ l) : s ∈ (𝓝ˢ K) ×ˢ l

Full source

/-- 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.mem_nhdsSet_prod_of_forall {K : Set X} {Y} {l : Filter Y} {s : Set (X × Y)}
    (hK : IsCompact K) (hs : ∀ x ∈ K, s ∈ 𝓝 x ×ˢ l) : s ∈ (𝓝ˢ K) ×ˢ l := by
  refine hK.induction_on (by simp) (fun t t' ht hs ↦ ?_) (fun t t' ht ht' ↦ ?_) fun x hx ↦ ?_
  · exact prod_mono (nhdsSet_mono ht) le_rfl hs
  · simp [sup_prod, *]
  · rcases ((nhds_basis_opens _).prod l.basis_sets).mem_iff.1 (hs x hx)
      with ⟨⟨u, v⟩, ⟨⟨hx, huo⟩, hv⟩, hs⟩
    refine ⟨u, nhdsWithin_le_nhds (huo.mem_nhds hx), mem_of_superset ?_ hs⟩
    exact prod_mem_prod (huo.mem_nhdsSet.2 Subset.rfl) hv

Compactness Criterion for Product Neighborhoods

Informal description

Let $X$ and $Y$ be topological spaces, $K \subseteq X$ a compact subset, $l$ a filter on $Y$, and $s \subseteq X \times Y$. If for every $x \in K$, the set $s$ belongs to the product neighborhood filter $\mathcal{N}_x \times l$, then $s$ belongs to the product filter $\mathcal{N}_K \times l$, where $\mathcal{N}_K$ is the neighborhood filter of $K$. In other words, there exist an open neighborhood $U$ of $K$ and a set $t \in l$ such that $U \times t \subseteq s$.

IsCompact.nhdsSet_prod_eq_biSup theorem

{K : Set X} (hK : IsCompact K) {Y} (l : Filter Y) : (𝓝ˢ K) ×ˢ l = ⨆ x ∈ K, 𝓝 x ×ˢ l

Full source

theorem IsCompact.nhdsSet_prod_eq_biSup {K : Set X} (hK : IsCompact K) {Y} (l : Filter Y) :
    (𝓝ˢ K) ×ˢ l = ⨆ x ∈ K, 𝓝 x ×ˢ l :=
  le_antisymm (fun s hs ↦ hK.mem_nhdsSet_prod_of_forall <| by simpa using hs)
    (iSup₂_le fun _ hx ↦ prod_mono (nhds_le_nhdsSet hx) le_rfl)

Product Filter Decomposition for Compact Sets: $\mathcal{N}_K \times l = \bigsqcup_{x \in K} (\mathcal{N}_x \times l)$

Informal description

Let $X$ and $Y$ be topological spaces, $K \subseteq X$ a compact subset, and $l$ a filter on $Y$. Then the product filter $\mathcal{N}_K \times l$ (where $\mathcal{N}_K$ is the neighborhood filter of $K$) is equal to the supremum of the product filters $\mathcal{N}_x \times l$ for all $x \in K$, i.e., \[ \mathcal{N}_K \times l = \bigsqcup_{x \in K} (\mathcal{N}_x \times l). \]

IsCompact.prod_nhdsSet_eq_biSup theorem

{K : Set Y} (hK : IsCompact K) {X} (l : Filter X) : l ×ˢ (𝓝ˢ K) = ⨆ y ∈ K, l ×ˢ 𝓝 y

Full source

theorem IsCompact.prod_nhdsSet_eq_biSup {K : Set Y} (hK : IsCompact K) {X} (l : Filter X) :
    l ×ˢ (𝓝ˢ K) = ⨆ y ∈ K, l ×ˢ 𝓝 y := by
  simp only [prod_comm (f := l), hK.nhdsSet_prod_eq_biSup, map_iSup]

Product Filter Decomposition for Compact Sets: $l \times \mathcal{N}_K = \bigsqcup_{y \in K} (l \times \mathcal{N}_y)$

Informal description

Let $X$ and $Y$ be topological spaces, $K \subseteq Y$ a compact subset, and $l$ a filter on $X$. Then the product filter $l \times \mathcal{N}_K$ (where $\mathcal{N}_K$ is the neighborhood filter of $K$) is equal to the supremum of the product filters $l \times \mathcal{N}_y$ for all $y \in K$, i.e., \[ l \times \mathcal{N}_K = \bigsqcup_{y \in K} (l \times \mathcal{N}_y). \]

IsCompact.mem_prod_nhdsSet_of_forall theorem

 {K : Set Y} {X} {l : Filter X} {s : Set (X × Y)} (hK : IsCompact K) (hs : ∀ y ∈ K, s ∈ l ×ˢ 𝓝 y) : s ∈ l ×ˢ 𝓝ˢ K

Full source

/-- 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.mem_prod_nhdsSet_of_forall {K : Set Y} {X} {l : Filter X} {s : Set (X × Y)}
    (hK : IsCompact K) (hs : ∀ y ∈ K, s ∈ l ×ˢ 𝓝 y) : s ∈ l ×ˢ 𝓝ˢ K :=
  (hK.prod_nhdsSet_eq_biSup l).symm ▸ by simpa using hs

Inclusion in Product Filter via Compactness: $s \in l \times \mathcal{N}_K$ from Local Conditions

Informal description

Let $X$ and $Y$ be topological spaces, $K \subseteq Y$ a compact subset, $l$ a filter on $X$, and $s \subseteq X \times Y$ a set. If for every $y \in K$, the set $s$ belongs to the product filter $l \times \mathcal{N}_y$ (where $\mathcal{N}_y$ is the neighborhood filter of $y$), then $s$ belongs to the product filter $l \times \mathcal{N}_K$ (where $\mathcal{N}_K$ is the neighborhood filter of $K$).

IsCompact.nhdsSet_inf_eq_biSup theorem

{K : Set X} (hK : IsCompact K) (l : Filter X) : (𝓝ˢ K) ⊓ l = ⨆ x ∈ K, 𝓝 x ⊓ l

Full source

theorem IsCompact.nhdsSet_inf_eq_biSup {K : Set X} (hK : IsCompact K) (l : Filter X) :
    (𝓝ˢ K) ⊓ l = ⨆ x ∈ K, 𝓝 x ⊓ l := by
  have : ∀ f : Filter X, f ⊓ l = comap (fun x ↦ (x, x)) (f ×ˢ l) := fun f ↦ by
    simpa only [comap_prod] using congrArg₂ (· ⊓ ·) comap_id.symm comap_id.symm
  simp_rw [this, ← comap_iSup, hK.nhdsSet_prod_eq_biSup]

Decomposition of Infimum with Neighborhood Filter of Compact Set: $\mathcal{N}_K \sqcap l = \bigsqcup_{x \in K} (\mathcal{N}_x \sqcap l)$

Informal description

Let $X$ be a topological space, $K \subseteq X$ a compact subset, and $l$ a filter on $X$. Then the infimum of the neighborhood filter $\mathcal{N}_K$ of $K$ with $l$ is equal to the supremum of the infima $\mathcal{N}_x \sqcap l$ for all $x \in K$, i.e., \[ \mathcal{N}_K \sqcap l = \bigsqcup_{x \in K} (\mathcal{N}_x \sqcap l). \]

IsCompact.inf_nhdsSet_eq_biSup theorem

{K : Set X} (hK : IsCompact K) (l : Filter X) : l ⊓ (𝓝ˢ K) = ⨆ x ∈ K, l ⊓ 𝓝 x

Full source

theorem IsCompact.inf_nhdsSet_eq_biSup {K : Set X} (hK : IsCompact K) (l : Filter X) :
    l ⊓ (𝓝ˢ K) = ⨆ x ∈ K, l ⊓ 𝓝 x := by
  simp only [inf_comm l, hK.nhdsSet_inf_eq_biSup]

Decomposition of Infimum with Neighborhood Filter of Compact Set (Symmetric Version)

Informal description

Let $X$ be a topological space, $K \subseteq X$ a compact subset, and $l$ a filter on $X$. Then the infimum of $l$ with the neighborhood filter $\mathcal{N}_K$ of $K$ is equal to the supremum of the infima $l \sqcap \mathcal{N}_x$ for all $x \in K$, i.e., \[ l \sqcap \mathcal{N}_K = \bigsqcup_{x \in K} (l \sqcap \mathcal{N}_x). \]

IsCompact.mem_nhdsSet_inf_of_forall theorem

 {K : Set X} {l : Filter X} {s : Set X} (hK : IsCompact K) (hs : ∀ x ∈ K, s ∈ 𝓝 x ⊓ l) : s ∈ (𝓝ˢ K) ⊓ l

Full source

/-- 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_nhdsSet_inf_of_forall {K : Set X} {l : Filter X} {s : Set X}
    (hK : IsCompact K) (hs : ∀ x ∈ K, s ∈ 𝓝 x ⊓ l) : s ∈ (𝓝ˢ K) ⊓ l :=
  (hK.nhdsSet_inf_eq_biSup l).symm ▸ by simpa using hs

Inclusion in Infimum of Neighborhood Filter of Compact Set via Pointwise Condition

Informal description

Let $X$ be a topological space, $K \subseteq X$ a compact subset, $l$ a filter on $X$, and $s \subseteq X$. If for every $x \in K$, the set $s$ belongs to the infimum of the neighborhood filter $\mathcal{N}_x$ and $l$, then $s$ belongs to the infimum of the neighborhood filter $\mathcal{N}_K$ of $K$ and $l$. In other words, if $s \in \mathcal{N}_x \sqcap l$ for all $x \in K$, then $s \in \mathcal{N}_K \sqcap l$.

IsCompact.mem_inf_nhdsSet_of_forall theorem

{K : Set X} {l : Filter X} {s : Set X} (hK : IsCompact K) (hs : ∀ y ∈ K, s ∈ l ⊓ 𝓝 y) : s ∈ l ⊓ 𝓝ˢ K

Full source

/-- 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.mem_inf_nhdsSet_of_forall {K : Set X} {l : Filter X} {s : Set X}
    (hK : IsCompact K) (hs : ∀ y ∈ K, s ∈ l ⊓ 𝓝 y) : s ∈ l ⊓ 𝓝ˢ K :=
  (hK.inf_nhdsSet_eq_biSup l).symm ▸ by simpa using hs

Inclusion in Infimum of Filter and Neighborhood Filter of Compact Set via Pointwise Condition

Informal description

Let $X$ be a topological space, $K \subseteq X$ a compact subset, $l$ a filter on $X$, and $s \subseteq X$. If for every $y \in K$, the set $s$ belongs to the infimum of $l$ and the neighborhood filter $\mathcal{N}_y$ of $y$, then $s$ belongs to the infimum of $l$ and the neighborhood filter $\mathcal{N}_K$ of $K$. In other words, if $s \in l \sqcap \mathcal{N}_y$ for all $y \in K$, then $s \in l \sqcap \mathcal{N}_K$.

IsCompact.eventually_forall_of_forall_eventually theorem

 {x₀ : X} {K : Set Y} (hK : IsCompact K) {P : X → Y → Prop} (hP : ∀ y ∈ K, ∀ᶠ z : X × Y in 𝓝 (x₀, y), P z.1 z.2) :
  ∀ᶠ x in 𝓝 x₀, ∀ y ∈ K, P x y

Full source

/-- To show that `∀ y ∈ K, P x y` holds for `x` close enough to `x₀` when `K` is compact,
it is sufficient to show that for all `y₀ ∈ K` there `P x y` holds for `(x, y)` close enough
to `(x₀, y₀)`.

Provided for backwards compatibility,
see `IsCompact.mem_prod_nhdsSet_of_forall` for a stronger statement.
-/
theorem IsCompact.eventually_forall_of_forall_eventually {x₀ : X} {K : Set Y} (hK : IsCompact K)
    {P : X → Y → Prop} (hP : ∀ y ∈ K, ∀ᶠ z : X × Y in 𝓝 (x₀, y), P z.1 z.2) :
    ∀ᶠ x in 𝓝 x₀, ∀ y ∈ K, P x y := by
  simp only [nhds_prod_eq, ← eventually_iSup, ← hK.prod_nhdsSet_eq_biSup] at hP
  exact hP.curry.mono fun _ h ↦ h.self_of_nhdsSet

Uniform Continuity of Predicates over Compact Sets

Informal description

Let $X$ and $Y$ be topological spaces, $x_0 \in X$, and $K \subseteq Y$ a compact subset. For a predicate $P : X \to Y \to \text{Prop}$, if for every $y \in K$ the property $P(x,y)$ holds for all $(x,y)$ in some neighborhood of $(x_0,y)$, then there exists a neighborhood of $x_0$ such that for all $x$ in this neighborhood and all $y \in K$, the property $P(x,y)$ holds. In other words: \[ \left( \forall y \in K, \exists U \in \mathcal{N}(x_0,y), \forall (x,y) \in U, P(x,y) \right) \implies \exists V \in \mathcal{N}(x_0), \forall x \in V, \forall y \in K, P(x,y). \]

isCompact_empty theorem

: IsCompact (∅ : Set X)

Full source

theorem isCompact_empty : IsCompact (∅ : Set X) := fun _f hnf hsf =>
  Not.elim hnf.ne <| empty_mem_iff_bot.1 <| le_principal_iff.1 hsf

Compactness of the Empty Set

Informal description

The empty set is compact in any topological space $X$.

isCompact_singleton theorem

{x : X} : IsCompact ({ x } : Set X)

Full source

theorem isCompact_singleton {x : X} : IsCompact ({x} : Set X) := fun _ hf hfa =>
  ⟨x, rfl, ClusterPt.of_le_nhds'
    (hfa.trans <| by simpa only [principal_singleton] using pure_le_nhds x) hf⟩

Compactness of Singleton Sets

Informal description

For any point $x$ in a topological space $X$, the singleton set $\{x\}$ is compact.

Set.Subsingleton.isCompact theorem

(hs : s.Subsingleton) : IsCompact s

Full source

theorem Set.Subsingleton.isCompact (hs : s.Subsingleton) : IsCompact s :=
  Subsingleton.induction_on hs isCompact_empty fun _ => isCompact_singleton

Compactness of Subsingleton Sets

Informal description

For any subset $s$ of a topological space $X$, if $s$ is a subsingleton (i.e., contains at most one element), then $s$ is compact.

Set.Finite.isCompact_biUnion theorem

{s : Set ι} {f : ι → Set X} (hs : s.Finite) (hf : ∀ i ∈ s, IsCompact (f i)) : IsCompact (⋃ i ∈ s, f i)

Full source

theorem Set.Finite.isCompact_biUnion {s : Set ι} {f : ι → Set X} (hs : s.Finite)
    (hf : ∀ i ∈ s, IsCompact (f i)) : IsCompact (⋃ i ∈ s, f i) :=
  isCompact_iff_ultrafilter_le_nhds'.2 fun l hl => by
    rw [Ultrafilter.finite_biUnion_mem_iff hs] at hl
    rcases hl with ⟨i, his, hi⟩
    rcases (hf i his).ultrafilter_le_nhds _ (le_principal_iff.2 hi) with ⟨x, hxi, hlx⟩
    exact ⟨x, mem_iUnion₂.2 ⟨i, his, hxi⟩, hlx⟩

Finite Union of Compact Sets is Compact

Informal description

Let $X$ be a topological space and $\iota$ an index set. For any finite subset $s \subseteq \iota$ and any family of compact sets $\{f(i)\}_{i \in s}$ in $X$, the union $\bigcup_{i \in s} f(i)$ is compact.

Finset.isCompact_biUnion theorem

(s : Finset ι) {f : ι → Set X} (hf : ∀ i ∈ s, IsCompact (f i)) : IsCompact (⋃ i ∈ s, f i)

Full source

theorem Finset.isCompact_biUnion (s : Finset ι) {f : ι → Set X} (hf : ∀ i ∈ s, IsCompact (f i)) :
    IsCompact (⋃ i ∈ s, f i) :=
  s.finite_toSet.isCompact_biUnion hf

Finite Union of Compact Sets is Compact (Finset Version)

Informal description

Let $X$ be a topological space and $\iota$ an index set. For any finite subset $s \subseteq \iota$ (represented as a finset) and any family of compact sets $\{f(i)\}_{i \in s}$ in $X$, the union $\bigcup_{i \in s} f(i)$ is compact.

isCompact_accumulate theorem

{K : ℕ → Set X} (hK : ∀ n, IsCompact (K n)) (n : ℕ) : IsCompact (Accumulate K n)

Full source

theorem isCompact_accumulate {K : ℕ → Set X} (hK : ∀ n, IsCompact (K n)) (n : ℕ) :
    IsCompact (Accumulate K n) :=
  (finite_le_nat n).isCompact_biUnion fun k _ => hK k

Compactness of Accumulated Sets in a Sequence of Compact Sets

Informal description

For any sequence of compact sets $\{K(n)\}_{n \in \mathbb{N}}$ in a topological space $X$ and for any natural number $n$, the accumulated set $\text{Accumulate}(K, n)$ is compact.

Set.Finite.isCompact_sUnion theorem

{S : Set (Set X)} (hf : S.Finite) (hc : ∀ s ∈ S, IsCompact s) : IsCompact (⋃₀ S)

Full source

theorem Set.Finite.isCompact_sUnion {S : Set (Set X)} (hf : S.Finite) (hc : ∀ s ∈ S, IsCompact s) :
    IsCompact (⋃₀ S) := by
  rw [sUnion_eq_biUnion]; exact hf.isCompact_biUnion hc

Finite Union of Compact Sets is Compact (Set Version)

Informal description

Let $X$ be a topological space and $S$ be a finite collection of subsets of $X$. If every set in $S$ is compact, then the union of all sets in $S$ is compact.

isCompact_iUnion theorem

{ι : Sort*} {f : ι → Set X} [Finite ι] (h : ∀ i, IsCompact (f i)) : IsCompact (⋃ i, f i)

Full source

theorem isCompact_iUnion {ι : Sort*} {f : ι → Set X} [Finite ι] (h : ∀ i, IsCompact (f i)) :
    IsCompact (⋃ i, f i) :=
  (finite_range f).isCompact_sUnion <| forall_mem_range.2 h

Finite Union of Compact Sets is Compact (Indexed Version)

Informal description

Let $X$ be a topological space and $\{f_i\}_{i \in \iota}$ be a finite family of subsets of $X$. If each $f_i$ is compact, then their union $\bigcup_{i \in \iota} f_i$ is compact.

Set.Finite.isCompact theorem

(hs : s.Finite) : IsCompact s

Full source

@[simp] theorem Set.Finite.isCompact (hs : s.Finite) : IsCompact s :=
  biUnion_of_singleton s ▸ hs.isCompact_biUnion fun _ _ => isCompact_singleton

Finite Sets are Compact

Informal description

For any finite subset $s$ of a topological space $X$, the set $s$ is compact.

IsCompact.finite_of_discrete theorem

[DiscreteTopology X] (hs : IsCompact s) : s.Finite

Full source

theorem IsCompact.finite_of_discrete [DiscreteTopology X] (hs : IsCompact s) : s.Finite := by
  have : ∀ x : X, ({x} : Set X) ∈ 𝓝 x := by simp [nhds_discrete]
  rcases hs.elim_nhds_subcover (fun x => {x}) fun x _ => this x with ⟨t, _, hst⟩
  simp only [← t.set_biUnion_coe, biUnion_of_singleton] at hst
  exact t.finite_toSet.subset hst

Compact subsets in discrete spaces are finite

Informal description

Let $X$ be a topological space with the discrete topology. If a subset $s \subseteq X$ is compact, then $s$ is finite.

isCompact_iff_finite theorem

[DiscreteTopology X] : IsCompact s ↔ s.Finite

Full source

theorem isCompact_iff_finite [DiscreteTopology X] : IsCompactIsCompact s ↔ s.Finite :=
  ⟨fun h => h.finite_of_discrete, fun h => h.isCompact⟩

Compactness Characterization in Discrete Spaces: Finite if and only if Compact

Informal description

Let $X$ be a topological space with the discrete topology. A subset $s \subseteq X$ is compact if and only if $s$ is finite.

IsCompact.union theorem

(hs : IsCompact s) (ht : IsCompact t) : IsCompact (s ∪ t)

Full source

theorem IsCompact.union (hs : IsCompact s) (ht : IsCompact t) : IsCompact (s ∪ t) := by
  rw [union_eq_iUnion]; exact isCompact_iUnion fun b => by cases b <;> assumption

Union of Two Compact Sets is Compact

Informal description

If $s$ and $t$ are compact subsets of a topological space $X$, then their union $s \cup t$ is also compact.

IsCompact.insert theorem

(hs : IsCompact s) (a) : IsCompact (insert a s)

Full source

protected theorem IsCompact.insert (hs : IsCompact s) (a) : IsCompact (insert a s) :=
  isCompact_singleton.union hs

Compactness of Union with Singleton Set

Informal description

If $s$ is a compact subset of a topological space $X$ and $a$ is a point in $X$, then the set $\{a\} \cup s$ is compact.

exists_subset_nhds_of_isCompact' theorem

 [Nonempty ι] {V : ι → Set X} (hV : Directed (· ⊇ ·) V) (hV_cpct : ∀ i, IsCompact (V i))
  (hV_closed : ∀ i, IsClosed (V i)) {U : Set X} (hU : ∀ x ∈ ⋂ i, V i, U ∈ 𝓝 x) : ∃ i, V i ⊆ U

Full source

/-- 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 exists_subset_nhds_of_isCompact' [Nonempty ι] {V : ι → Set X}
    (hV : Directed (· ⊇ ·) V) (hV_cpct : ∀ i, IsCompact (V i)) (hV_closed : ∀ i, IsClosed (V i))
    {U : Set X} (hU : ∀ x ∈ ⋂ i, V i, U ∈ 𝓝 x) : ∃ i, V i ⊆ U := by
  obtain ⟨W, hsubW, W_op, hWU⟩ := exists_open_set_nhds hU
  suffices ∃ i, V i ⊆ W from this.imp fun i hi => hi.trans hWU
  by_contra! H
  replace H : ∀ i, (V i ∩ Wᶜ).Nonempty := fun i => Set.inter_compl_nonempty_iff.mpr (H i)
  have : (⋂ i, V i ∩ Wᶜ).Nonempty := by
    refine
      IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed _ (fun i j => ?_) H
        (fun i => (hV_cpct i).inter_right W_op.isClosed_compl) fun i =>
        (hV_closed i).inter W_op.isClosed_compl
    rcases hV i j with ⟨k, hki, hkj⟩
    refine ⟨k, ⟨fun x => ?_, fun x => ?_⟩⟩ <;> simp only [and_imp, mem_inter_iff, mem_compl_iff] <;>
      tauto
  have : ¬⋂ i : ι, V i ⊆ W := by simpa [← iInter_inter, inter_compl_nonempty_iff]
  contradiction

Neighborhood Containment Property for Directed Families of Compact Closed Sets

Informal description

Let $X$ be a topological space and $\{V_i\}_{i \in \iota}$ a nonempty directed family of compact closed subsets of $X$ with respect to reverse inclusion ($\supseteq$). If $U$ is a neighborhood of the intersection $\bigcap_{i \in \iota} V_i$ (i.e., for every $x \in \bigcap_{i \in \iota} V_i$, $U$ contains an open neighborhood of $x$), then there exists some index $i$ such that $V_i \subseteq U$.

Filter.hasBasis_cocompact theorem

: (cocompact X).HasBasis IsCompact compl

Full source

theorem hasBasis_cocompact : (cocompact X).HasBasis IsCompact compl :=
  hasBasis_biInf_principal'
    (fun s hs t ht =>
      ⟨s ∪ t, hs.union ht, compl_subset_compl.2 subset_union_left,
        compl_subset_compl.2 subset_union_right⟩)
    ⟨∅, isCompact_empty⟩

Cocompact Filter Basis Characterization

Informal description

The cocompact filter on a topological space $X$ has a basis consisting of the complements of all compact subsets of $X$. In other words, a set $s$ belongs to the cocompact filter if and only if it contains the complement of some compact set $t$ in $X$.

Filter.mem_cocompact theorem

: s ∈ cocompact X ↔ ∃ t, IsCompact t ∧ tᶜ ⊆ s

Full source

theorem mem_cocompact : s ∈ cocompact Xs ∈ cocompact X ↔ ∃ t, IsCompact t ∧ tᶜ ⊆ s :=
  hasBasis_cocompact.mem_iff

Characterization of Cocompact Filter Membership via Compact Sets

Informal description

A set $s$ in a topological space $X$ belongs to the cocompact filter if and only if there exists a compact subset $t \subseteq X$ such that the complement of $t$ is contained in $s$.

Filter.mem_cocompact' theorem

: s ∈ cocompact X ↔ ∃ t, IsCompact t ∧ sᶜ ⊆ t

Full source

theorem mem_cocompact' : s ∈ cocompact Xs ∈ cocompact X ↔ ∃ t, IsCompact t ∧ sᶜ ⊆ t :=
  mem_cocompact.trans <| exists_congr fun _ => and_congr_right fun _ => compl_subset_comm

Characterization of Cocompact Filter Membership via Complement Containment

Informal description

A set $s$ in a topological space $X$ belongs to the cocompact filter if and only if there exists a compact subset $t \subseteq X$ such that the complement of $s$ is contained in $t$.

IsCompact.compl_mem_cocompact theorem

(hs : IsCompact s) : sᶜ ∈ Filter.cocompact X

Full source

theorem _root_.IsCompact.compl_mem_cocompact (hs : IsCompact s) : sᶜsᶜ ∈ Filter.cocompact X :=
  hasBasis_cocompact.mem_of_mem hs

Complement of Compact Set Belongs to Cocompact Filter

Informal description

If $s$ is a compact subset of a topological space $X$, then its complement $s^c$ belongs to the cocompact filter on $X$.

Filter.cocompact_le_cofinite theorem

: cocompact X ≤ cofinite

Full source

theorem cocompact_le_cofinite : cocompact X ≤ cofinite := fun s hs =>
  compl_compl s ▸ hs.isCompact.compl_mem_cocompact

Cocompact Filter is Finer than Cofinite Filter

Informal description

For any topological space $X$, the cocompact filter is finer than the cofinite filter. That is, every subset with finite complement is also cocompact.

Filter.cocompact_eq_cofinite theorem

(X : Type*) [TopologicalSpace X] [DiscreteTopology X] : cocompact X = cofinite

Full source

theorem cocompact_eq_cofinite (X : Type*) [TopologicalSpace X] [DiscreteTopology X] :
    cocompact X = cofinite := by
  simp only [cocompact, hasBasis_cofinite.eq_biInf, isCompact_iff_finite]

Cocompact Filter Equals Cofinite Filter in Discrete Spaces

Informal description

For any topological space $X$ with the discrete topology, the cocompact filter on $X$ is equal to the cofinite filter. That is, a subset $s \subseteq X$ has compact complement if and only if its complement is finite.

Filter.disjoint_cocompact_left theorem

(f : Filter X) : Disjoint (Filter.cocompact X) f ↔ ∃ K ∈ f, IsCompact K

Full source

/-- A filter is disjoint from the cocompact filter if and only if it contains a compact set. -/
theorem disjoint_cocompact_left (f : Filter X) :
    DisjointDisjoint (Filter.cocompact X) f ↔ ∃ K ∈ f, IsCompact K := by
  simp_rw [hasBasis_cocompact.disjoint_iff_left, compl_compl]
  tauto

Disjointness from Cocompact Filter is Equivalent to Containing a Compact Set

Informal description

A filter $f$ on a topological space $X$ is disjoint from the cocompact filter if and only if there exists a compact set $K$ that belongs to $f$.

Filter.disjoint_cocompact_right theorem

(f : Filter X) : Disjoint f (Filter.cocompact X) ↔ ∃ K ∈ f, IsCompact K

Full source

/-- A filter is disjoint from the cocompact filter if and only if it contains a compact set. -/
theorem disjoint_cocompact_right (f : Filter X) :
    DisjointDisjoint f (Filter.cocompact X) ↔ ∃ K ∈ f, IsCompact K := by
  simp_rw [hasBasis_cocompact.disjoint_iff_right, compl_compl]
  tauto

Disjointness with Cocompact Filter Characterized by Compact Sets

Informal description

A filter $f$ on a topological space $X$ is disjoint from the cocompact filter if and only if there exists a compact set $K$ that belongs to $f$.

Filter.Tendsto.isCompact_insert_range_of_cocompact theorem

{f : X → Y} {y} (hf : Tendsto f (cocompact X) (𝓝 y)) (hfc : Continuous f) : IsCompact (insert y (range f))

Full source

theorem Tendsto.isCompact_insert_range_of_cocompact {f : X → Y} {y}
    (hf : Tendsto f (cocompact X) (𝓝 y)) (hfc : Continuous f) : IsCompact (insert y (range f)) := by
  intro l hne hle
  by_cases hy : ClusterPt y l
  · exact ⟨y, Or.inl rfl, hy⟩
  simp only [clusterPt_iff_nonempty, not_forall, ← not_disjoint_iff_nonempty_inter, not_not] at hy
  rcases hy with ⟨s, hsy, t, htl, hd⟩
  rcases mem_cocompact.1 (hf hsy) with ⟨K, hKc, hKs⟩
  have : f '' Kf '' K ∈ l := by
    filter_upwards [htl, le_principal_iff.1 hle] with y hyt hyf
    rcases hyf with (rfl | ⟨x, rfl⟩)
    exacts [(hd.le_bot ⟨mem_of_mem_nhds hsy, hyt⟩).elim,
      mem_image_of_mem _ (not_not.1 fun hxK => hd.le_bot ⟨hKs hxK, hyt⟩)]
  rcases hKc.image hfc (le_principal_iff.2 this) with ⟨y, hy, hyl⟩
  exact ⟨y, Or.inr <| image_subset_range _ _ hy, hyl⟩

Compactness of Extended Range under Cocompact Convergence

Informal description

Let $X$ and $Y$ be topological spaces, $f : X \to Y$ a continuous function, and $y \in Y$. If $f$ tends to $y$ along the cocompact filter of $X$, then the set obtained by inserting $y$ into the range of $f$ is compact in $Y$.

Filter.Tendsto.isCompact_insert_range_of_cofinite theorem

{f : ι → X} {x} (hf : Tendsto f cofinite (𝓝 x)) : IsCompact (insert x (range f))

Full source

theorem Tendsto.isCompact_insert_range_of_cofinite {f : ι → X} {x} (hf : Tendsto f cofinite (𝓝 x)) :
    IsCompact (insert x (range f)) := by
  letI : TopologicalSpace ι := ⊥; haveI h : DiscreteTopology ι := ⟨rfl⟩
  rw [← cocompact_eq_cofinite ι] at hf
  exact hf.isCompact_insert_range_of_cocompact continuous_of_discreteTopology

Compactness of extended range under cofinite convergence

Informal description

Let $X$ be a topological space, $f : \iota \to X$ a function, and $x \in X$. If $f$ tends to $x$ along the cofinite filter, then the set obtained by inserting $x$ into the range of $f$ is compact in $X$.

Filter.Tendsto.isCompact_insert_range theorem

{f : ℕ → X} {x} (hf : Tendsto f atTop (𝓝 x)) : IsCompact (insert x (range f))

Full source

theorem Tendsto.isCompact_insert_range {f : ℕ → X} {x} (hf : Tendsto f atTop (𝓝 x)) :
    IsCompact (insert x (range f)) :=
  Filter.Tendsto.isCompact_insert_range_of_cofinite <| Nat.cofinite_eq_atTop.symm ▸ hf

Compactness of Extended Range of a Convergent Sequence

Informal description

Let $X$ be a topological space, $f : \mathbb{N} \to X$ a sequence, and $x \in X$. If $f$ converges to $x$ in the topology of $X$, then the set obtained by inserting $x$ into the range of $f$ is compact in $X$.

Filter.hasBasis_coclosedCompact theorem

: (Filter.coclosedCompact X).HasBasis (fun s => IsClosed s ∧ IsCompact s) compl

Full source

theorem hasBasis_coclosedCompact :
    (Filter.coclosedCompact X).HasBasis (fun s => IsClosedIsClosed s ∧ IsCompact s) compl := by
  simp only [Filter.coclosedCompact, iInf_and']
  refine hasBasis_biInf_principal' ?_ ⟨∅, isClosed_empty, isCompact_empty⟩
  rintro s ⟨hs₁, hs₂⟩ t ⟨ht₁, ht₂⟩
  exact ⟨s ∪ t, ⟨⟨hs₁.union ht₁, hs₂.union ht₂⟩, compl_subset_compl.2 subset_union_left,
    compl_subset_compl.2 subset_union_right⟩⟩

Basis Characterization of the Coclosed-Compact Filter

Informal description

The filter `coclosedCompact` on a topological space $X$ has a basis consisting of the complements of all subsets $s \subseteq X$ that are both closed and compact. In other words, a set belongs to `coclosedCompact X` if and only if it is the complement of a closed and compact subset of $X$.

Filter.mem_coclosedCompact_iff theorem

: s ∈ coclosedCompact X ↔ IsCompact (closure sᶜ)

Full source

/-- A set belongs to `coclosedCompact` if and only if the closure of its complement is compact. -/
theorem mem_coclosedCompact_iff :
    s ∈ coclosedCompact Xs ∈ coclosedCompact X ↔ IsCompact (closure sᶜ) := by
  refine hasBasis_coclosedCompact.mem_iff.trans ⟨?_, fun h ↦ ?_⟩
  · rintro ⟨t, ⟨htcl, htco⟩, hst⟩
    exact htco.of_isClosed_subset isClosed_closure <|
      closure_minimal (compl_subset_comm.2 hst) htcl
  · exact ⟨closure sᶜ, ⟨isClosed_closure, h⟩, compl_subset_comm.2 subset_closure⟩

Characterization of Coclosed-Compact Sets via Complement Closure

Informal description

A subset $s$ of a topological space $X$ belongs to the coclosed-compact filter if and only if the closure of its complement $s^c$ is compact.

Filter.compl_mem_coclosedCompact theorem

: sᶜ ∈ coclosedCompact X ↔ IsCompact (closure s)

Full source

/-- Complement of a set belongs to `coclosedCompact` if and only if its closure is compact. -/
theorem compl_mem_coclosedCompact : sᶜsᶜ ∈ coclosedCompact Xsᶜ ∈ coclosedCompact X ↔ IsCompact (closure s) := by
  rw [mem_coclosedCompact_iff, compl_compl]

Characterization of Coclosed-Compact Membership via Complement Closure: $s^c \in \text{coclosedCompact}(X) \leftrightarrow \text{IsCompact}(\overline{s})$

Informal description

For any subset $s$ of a topological space $X$, the complement $s^c$ belongs to the coclosed-compact filter if and only if the closure of $s$ is compact. In other words, $s^c \in \text{coclosedCompact}(X) \leftrightarrow \text{IsCompact}(\overline{s})$.

Filter.cocompact_le_coclosedCompact theorem

: cocompact X ≤ coclosedCompact X

Full source

theorem cocompact_le_coclosedCompact : cocompact X ≤ coclosedCompact X :=
  iInf_mono fun _ => le_iInf fun _ => le_rfl

Cocompact filter is finer than coclosed-compact filter

Informal description

The cocompact filter on a topological space $X$ is finer than the coclosed-compact filter on $X$, i.e., $\text{cocompact}(X) \leq \text{coclosedCompact}(X)$.

IsCompact.compl_mem_coclosedCompact_of_isClosed theorem

(hs : IsCompact s) (hs' : IsClosed s) : sᶜ ∈ Filter.coclosedCompact X

Full source

theorem IsCompact.compl_mem_coclosedCompact_of_isClosed (hs : IsCompact s) (hs' : IsClosed s) :
    sᶜsᶜ ∈ Filter.coclosedCompact X :=
  hasBasis_coclosedCompact.mem_of_mem ⟨hs', hs⟩

Complement of Closed-Compact Set Belongs to Coclosed-Compact Filter

Informal description

For any closed and compact subset $s$ of a topological space $X$, the complement $s^c$ belongs to the coclosed-compact filter on $X$.

Bornology.inCompact definition

: Bornology X

Full source

/-- 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. -/
def inCompact : Bornology X where
  cobounded' := Filter.cocompact X
  le_cofinite' := Filter.cocompact_le_cofinite

Bornology of relatively compact sets

Informal description

The bornology on a topological space $X$ where a set is bounded if and only if it is contained in a compact set. The cobounded filter for this bornology is the cocompact filter, which consists of subsets with compact complement.

Bornology.inCompact.isBounded_iff theorem

: @IsBounded _ (inCompact X) s ↔ ∃ t, IsCompact t ∧ s ⊆ t

Full source

theorem inCompact.isBounded_iff : @IsBounded _ (inCompact X) s ↔ ∃ t, IsCompact t ∧ s ⊆ t := by
  change sᶜsᶜ ∈ Filter.cocompact Xsᶜ ∈ Filter.cocompact X ↔ _
  rw [Filter.mem_cocompact]
  simp

Characterization of Bounded Sets in the Bornology of Relatively Compact Sets

Informal description

A subset $s$ of a topological space $X$ is bounded with respect to the bornology of relatively compact sets if and only if there exists a compact subset $t$ of $X$ such that $s \subseteq t$.

IsCompact.nhdsSet_prod_eq theorem

{t : Set Y} (hs : IsCompact s) (ht : IsCompact t) : 𝓝ˢ (s ×ˢ t) = 𝓝ˢ s ×ˢ 𝓝ˢ t

Full source

/-- 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 IsCompact.nhdsSet_prod_eq {t : Set Y} (hs : IsCompact s) (ht : IsCompact t) :
    𝓝ˢ (s ×ˢ t) = 𝓝ˢ s ×ˢ 𝓝ˢ t := by
  simp_rw [hs.nhdsSet_prod_eq_biSup, ht.prod_nhdsSet_eq_biSup, nhdsSet, sSup_image, biSup_prod,
    nhds_prod_eq]

Neighborhood Filter Equality for Product of Compact Sets: $\mathcal{N}_{s \times t} = \mathcal{N}_s \times \mathcal{N}_t$

Informal description

Let $X$ and $Y$ be topological spaces, and let $s \subseteq X$ and $t \subseteq Y$ be compact subsets. Then the neighborhood filter of the product set $s \times t$ is equal to the product of the neighborhood filters of $s$ and $t$, i.e., \[ \mathcal{N}_{s \times t} = \mathcal{N}_s \times \mathcal{N}_t. \]

nhdsSet_prod_le_of_disjoint_cocompact theorem

{f : Filter Y} (hs : IsCompact s) (hf : Disjoint f (Filter.cocompact Y)) : 𝓝ˢ s ×ˢ f ≤ 𝓝ˢ (s ×ˢ Set.univ)

Full source

theorem nhdsSet_prod_le_of_disjoint_cocompact {f : Filter Y} (hs : IsCompact s)
    (hf : Disjoint f (Filter.cocompact Y)) :
    𝓝ˢ s ×ˢ f ≤ 𝓝ˢ (s ×ˢ Set.univ) := by
  obtain ⟨K, hKf, hK⟩ := (disjoint_cocompact_right f).mp hf
  calc
    𝓝ˢ𝓝ˢ s ×ˢ f
    _ ≤ 𝓝ˢ s ×ˢ 𝓟 K        := Filter.prod_mono_right _ (Filter.le_principal_iff.mpr hKf)
    _ ≤ 𝓝ˢ s ×ˢ 𝓝ˢ K       := Filter.prod_mono_right _ principal_le_nhdsSet
    _ = 𝓝ˢ (s ×ˢ K)         := (hs.nhdsSet_prod_eq hK).symm
    _ ≤ 𝓝ˢ (s ×ˢ Set.univ)  := nhdsSet_mono (prod_mono_right le_top)

Product Filter Containment for Compact Set and Disjoint Cocompact Filter: $\mathcal{N}_s \times f \leq \mathcal{N}_{s \times Y}$

Informal description

Let $X$ and $Y$ be topological spaces, $s \subseteq X$ a compact subset, and $f$ a filter on $Y$ that is disjoint from the cocompact filter. Then the product filter $\mathcal{N}_s \times f$ is contained in the neighborhood filter of $s \times Y$, i.e., \[ \mathcal{N}_s \times f \leq \mathcal{N}_{s \times Y}. \]

prod_nhdsSet_le_of_disjoint_cocompact theorem

 {t : Set Y} {f : Filter X} (ht : IsCompact t) (hf : Disjoint f (Filter.cocompact X)) : f ×ˢ 𝓝ˢ t ≤ 𝓝ˢ (Set.univ ×ˢ t)

Full source

theorem prod_nhdsSet_le_of_disjoint_cocompact {t : Set Y} {f : Filter X} (ht : IsCompact t)
    (hf : Disjoint f (Filter.cocompact X)) :
    f ×ˢ 𝓝ˢ t ≤ 𝓝ˢ (Set.univ ×ˢ t) := by
  obtain ⟨K, hKf, hK⟩ := (disjoint_cocompact_right f).mp hf
  calc
    f ×ˢ 𝓝ˢ t
    _ ≤ (𝓟 K) ×ˢ 𝓝ˢ t      := Filter.prod_mono_left _ (Filter.le_principal_iff.mpr hKf)
    _ ≤ 𝓝ˢ K ×ˢ 𝓝ˢ t       := Filter.prod_mono_left _ principal_le_nhdsSet
    _ = 𝓝ˢ (K ×ˢ t)         := (hK.nhdsSet_prod_eq ht).symm
    _ ≤ 𝓝ˢ (Set.univ ×ˢ t)  := nhdsSet_mono (prod_mono_left le_top)

Product Filter Containment for Compact Set and Disjoint Cocompact Filter: $f \times \mathcal{N}_t \leq \mathcal{N}_{\text{univ} \times t}$

Informal description

Let $X$ and $Y$ be topological spaces, $t \subseteq Y$ be a compact subset, and $f$ be a filter on $X$ that is disjoint from the cocompact filter on $X$. Then the product filter $f \times \mathcal{N}_t$ is contained in the neighborhood filter of the set $\text{univ} \times t$, where $\text{univ}$ denotes the entire space $X$ and $\mathcal{N}_t$ is the neighborhood filter of $t$.

nhds_prod_le_of_disjoint_cocompact theorem

{f : Filter Y} (x : X) (hf : Disjoint f (Filter.cocompact Y)) : 𝓝 x ×ˢ f ≤ 𝓝ˢ ({ x } ×ˢ Set.univ)

Full source

theorem nhds_prod_le_of_disjoint_cocompact {f : Filter Y} (x : X)
    (hf : Disjoint f (Filter.cocompact Y)) :
    𝓝 x ×ˢ f ≤ 𝓝ˢ ({x} ×ˢ Set.univ) := by
  simpa using nhdsSet_prod_le_of_disjoint_cocompact isCompact_singleton hf

Product Filter Containment for Point and Disjoint Cocompact Filter: $\mathcal{N}_x \times f \leq \mathcal{N}_{\{x\} \times Y}$

Informal description

Let $X$ and $Y$ be topological spaces, $x \in X$ a point, and $f$ a filter on $Y$ that is disjoint from the cocompact filter on $Y$. Then the product filter $\mathcal{N}_x \times f$ is contained in the neighborhood filter of $\{x\} \times Y$, i.e., \[ \mathcal{N}_x \times f \leq \mathcal{N}_{\{x\} \times Y}. \]

prod_nhds_le_of_disjoint_cocompact theorem

{f : Filter X} (y : Y) (hf : Disjoint f (Filter.cocompact X)) : f ×ˢ 𝓝 y ≤ 𝓝ˢ (Set.univ ×ˢ { y })

Full source

theorem prod_nhds_le_of_disjoint_cocompact {f : Filter X} (y : Y)
    (hf : Disjoint f (Filter.cocompact X)) :
    f ×ˢ 𝓝 y ≤ 𝓝ˢ (Set.univ ×ˢ {y}) := by
  simpa using prod_nhdsSet_le_of_disjoint_cocompact isCompact_singleton hf

Product Filter Containment for Point and Disjoint Cocompact Filter: $f \times \mathcal{N}_y \leq \mathcal{N}_{X \times \{y\}}$

Informal description

Let $X$ and $Y$ be topological spaces, $y \in Y$ a point, and $f$ a filter on $X$ that is disjoint from the cocompact filter on $X$. Then the product filter $f \times \mathcal{N}_y$ is contained in the neighborhood filter of the set $X \times \{y\}$, where $\mathcal{N}_y$ is the neighborhood filter of $y$.

generalized_tube_lemma theorem

 (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

Full source

/-- If `s` and `t` are compact sets and `n` is an open neighborhood of `s × t`, then there exist
open neighborhoods `u ⊇ s` and `v ⊇ t` such that `u × v ⊆ n`.

See also `IsCompact.nhdsSet_prod_eq`. -/
theorem generalized_tube_lemma (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 := by
  rw [← hn.mem_nhdsSet, hs.nhdsSet_prod_eq ht,
    ((hasBasis_nhdsSet _).prod (hasBasis_nhdsSet _)).mem_iff] at hp
  rcases hp with ⟨⟨u, v⟩, ⟨⟨huo, hsu⟩, hvo, htv⟩, hn⟩
  exact ⟨u, v, huo, hvo, hsu, htv, hn⟩

Generalized Tube Lemma for Product of Compact Sets

Informal description

Let $X$ and $Y$ be topological spaces, and let $s \subseteq X$ and $t \subseteq Y$ be compact subsets. If $n$ is an open neighborhood of the product set $s \times t$, then there exist open neighborhoods $u \supseteq s$ and $v \supseteq t$ such that $u \times v \subseteq n$.

Subsingleton.compactSpace instance

[Subsingleton X] : CompactSpace X

Full source

instance (priority := 10) Subsingleton.compactSpace [Subsingleton X] : CompactSpace X :=
  ⟨subsingleton_univ.isCompact⟩

Compactness of Subsingleton Spaces

Informal description

Every subsingleton topological space is compact.

isCompact_univ_iff theorem

: IsCompact (univ : Set X) ↔ CompactSpace X

Full source

theorem isCompact_univ_iff : IsCompactIsCompact (univ : Set X) ↔ CompactSpace X :=
  ⟨fun h => ⟨h⟩, fun h => h.1⟩

Compactness of Universal Set Equivalence to Compact Space Property

Informal description

For a topological space $X$, the universal set $\text{univ} : \text{Set } X$ is compact if and only if $X$ is a compact space.

isCompact_univ theorem

[h : CompactSpace X] : IsCompact (univ : Set X)

Full source

theorem isCompact_univ [h : CompactSpace X] : IsCompact (univ : Set X) :=
  h.isCompact_univ

Compactness of the Universal Set in a Compact Space

Informal description

If $X$ is a compact space, then the universal set $\text{univ} \subseteq X$ is compact.

exists_clusterPt_of_compactSpace theorem

[CompactSpace X] (f : Filter X) [NeBot f] : ∃ x, ClusterPt x f

Full source

theorem exists_clusterPt_of_compactSpace [CompactSpace X] (f : Filter X) [NeBot f] :
    ∃ x, ClusterPt x f := by
  simpa using isCompact_univ (show f ≤ 𝓟 univ by simp)

Existence of Cluster Points in Compact Spaces

Informal description

If $X$ is a compact space and $f$ is a non-trivial filter on $X$, then there exists a point $x \in X$ that is a cluster point of $f$.

Ultrafilter.le_nhds_lim theorem

[CompactSpace X] (F : Ultrafilter X) : ↑F ≤ 𝓝 F.lim

Full source

nonrec theorem Ultrafilter.le_nhds_lim [CompactSpace X] (F : Ultrafilter X) : ↑F ≤ 𝓝 F.lim := by
  rcases isCompact_univ.ultrafilter_le_nhds F (by simp) with ⟨x, -, h⟩
  exact le_nhds_lim ⟨x, h⟩

Ultrafilter Convergence in Compact Spaces: $F \leq \mathcal{N}(F.\text{lim})$

Informal description

For any compact space $X$ and any ultrafilter $F$ on $X$, the ultrafilter $F$ converges to its limit point $F.\text{lim}$ in the neighborhood filter of $X$.

CompactSpace.elim_nhds_subcover theorem

[CompactSpace X] (U : X → Set X) (hU : ∀ x, U x ∈ 𝓝 x) : ∃ t : Finset X, ⋃ x ∈ t, U x = ⊤

Full source

theorem CompactSpace.elim_nhds_subcover [CompactSpace X] (U : X → Set X) (hU : ∀ x, U x ∈ 𝓝 x) :
    ∃ t : Finset X, ⋃ x ∈ t, U x = ⊤ := by
  obtain ⟨t, -, s⟩ := IsCompact.elim_nhds_subcover isCompact_univ U fun x _ => hU x
  exact ⟨t, top_unique s⟩

Finite Subcover Property for Compact Spaces: $\bigcup_{x \in t} U_x = X$

Informal description

Let $X$ be a compact topological space. For any family of open neighborhoods $\{U_x\}_{x \in X}$ such that $U_x$ is a neighborhood of $x$ for each $x \in X$, there exists a finite subset $t \subseteq X$ such that the union $\bigcup_{x \in t} U_x$ covers the entire space $X$.

compactSpace_of_finite_subfamily_closed theorem

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

Full source

theorem compactSpace_of_finite_subfamily_closed
    (h : ∀ {ι : Type u} (t : ι → Set X), (∀ i, IsClosed (t i)) → ⋂ i, t i = ∅ →
      ∃ u : Finset ι, ⋂ i ∈ u, t i = ∅) :
    CompactSpace X where
  isCompact_univ := isCompact_of_finite_subfamily_closed fun t => by simpa using h t

Compactness Criterion via Finite Subfamily of Closed Sets

Informal description

A topological space $X$ is compact if for every family of closed sets $(t_i)_{i \in \iota}$ such that their intersection is empty (i.e., $\bigcap_{i \in \iota} t_i = \emptyset$), there exists a finite subset of indices $u \subseteq \iota$ such that the intersection of the corresponding finite subfamily $(t_i)_{i \in u}$ is still empty (i.e., $\bigcap_{i \in u} t_i = \emptyset$).

IsClosed.isCompact theorem

[CompactSpace X] (h : IsClosed s) : IsCompact s

Full source

theorem IsClosed.isCompact [CompactSpace X] (h : IsClosed s) : IsCompact s :=
  isCompact_univ.of_isClosed_subset h (subset_univ _)

Closed Subsets are Compact in Compact Spaces

Informal description

In a compact topological space $X$, every closed subset $s \subseteq X$ is compact.

le_nhds_of_unique_clusterPt theorem

[CompactSpace X] {l : Filter X} {y : X} (h : ∀ x, ClusterPt x l → x = y) : l ≤ 𝓝 y

Full source

/-- If a filter has a unique cluster point `y` in a compact topological space,
then the filter is less than or equal to `𝓝 y`. -/
lemma le_nhds_of_unique_clusterPt [CompactSpace X] {l : Filter X} {y : X}
    (h : ∀ x, ClusterPt x l → x = y) : l ≤ 𝓝 y :=
  isCompact_univ.le_nhds_of_unique_clusterPt univ_mem fun x _ ↦ h x

Convergence of Filter with Unique Cluster Point in Compact Space

Informal description

Let $X$ be a compact topological space, and let $l$ be a filter on $X$. If $y \in X$ is the unique cluster point of $l$ (i.e., for all $x \in X$, if $x$ is a cluster point of $l$ then $x = y$), then $l$ converges to $y$.

tendsto_nhds_of_unique_mapClusterPt theorem

 [CompactSpace X] {Y} {l : Filter Y} {y : X} {f : Y → X} (h : ∀ x, MapClusterPt x l f → x = y) : Tendsto f l (𝓝 y)

Full source

/-- 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`. -/
lemma tendsto_nhds_of_unique_mapClusterPt [CompactSpace X] {Y} {l : Filter Y} {y : X} {f : Y → X}
    (h : ∀ x, MapClusterPt x l f → x = y) :
    Tendsto f l (𝓝 y) :=
  le_nhds_of_unique_clusterPt h

Convergence to Unique Map Cluster Point in Compact Space

Informal description

Let $X$ be a compact topological space, $Y$ be a set, $l$ be a filter on $Y$, $y \in X$, and $f : Y \to X$ be a function. If $y$ is the unique map cluster point of $f$ along $l$ (i.e., for all $x \in X$, if $x$ is a map cluster point of $f$ along $l$ then $x = y$), then $f$ tends to $y$ along $l$.

noncompact_univ theorem

(X : Type*) [TopologicalSpace X] [NoncompactSpace X] : ¬IsCompact (univ : Set X)

Full source

lemma noncompact_univ (X : Type*) [TopologicalSpace X] [NoncompactSpace X] :
    ¬IsCompact (univ : Set X) :=
  NoncompactSpace.noncompact_univ

Noncompactness of Universal Set in Noncompact Spaces

Informal description

For any topological space $X$ that is noncompact, the universal set $\text{univ} \subseteq X$ is not compact.

IsCompact.ne_univ theorem

[NoncompactSpace X] (hs : IsCompact s) : s ≠ univ

Full source

theorem IsCompact.ne_univ [NoncompactSpace X] (hs : IsCompact s) : s ≠ univ := fun h =>
  noncompact_univ X (h ▸ hs)

Compact Subset Cannot Be Universal Set in Noncompact Space

Informal description

For any topological space $X$ that is noncompact, if a subset $s \subseteq X$ is compact, then $s$ is not equal to the universal set $\text{univ} \subseteq X$.

instNeBotCocompactOfNoncompactSpace instance

[NoncompactSpace X] : NeBot (Filter.cocompact X)

Full source

instance [NoncompactSpace X] : NeBot (Filter.cocompact X) := by
  refine Filter.hasBasis_cocompact.neBot_iff.2 fun hs => ?_
  contrapose hs; rw [not_nonempty_iff_eq_empty, compl_empty_iff] at hs
  rw [hs]; exact noncompact_univ X

Nontriviality of Cocompact Filter in Noncompact Spaces

Informal description

For any noncompact topological space $X$, the cocompact filter on $X$ is not the trivial filter.

Filter.cocompact_eq_bot theorem

[CompactSpace X] : Filter.cocompact X = ⊥

Full source

@[simp]
theorem Filter.cocompact_eq_bot [CompactSpace X] : Filter.cocompact X = ⊥ :=
  Filter.hasBasis_cocompact.eq_bot_iff.mpr ⟨Set.univ, isCompact_univ, Set.compl_univ⟩

Cocompact Filter is Trivial in Compact Spaces

Informal description

If $X$ is a compact space, then the cocompact filter on $X$ is equal to the trivial filter $\bot$.

instNeBotCoclosedCompactOfNoncompactSpace instance

[NoncompactSpace X] : NeBot (Filter.coclosedCompact X)

Full source

instance [NoncompactSpace X] : NeBot (Filter.coclosedCompact X) :=
  neBot_of_le Filter.cocompact_le_coclosedCompact

Nontriviality of Coclosed-Compact Filter in Noncompact Spaces

Informal description

For any noncompact topological space $X$, the coclosed-compact filter on $X$ is not the trivial filter.

noncompactSpace_of_neBot theorem

(_ : NeBot (Filter.cocompact X)) : NoncompactSpace X

Full source

theorem noncompactSpace_of_neBot (_ : NeBot (Filter.cocompact X)) : NoncompactSpace X :=
  ⟨fun h' => (Filter.nonempty_of_mem h'.compl_mem_cocompact).ne_empty compl_univ⟩

Noncompactness from Nontrivial Cocompact Filter

Informal description

If the cocompact filter on a topological space $X$ is not the trivial filter, then $X$ is a noncompact space.

Filter.cocompact_neBot_iff theorem

: NeBot (Filter.cocompact X) ↔ NoncompactSpace X

Full source

theorem Filter.cocompact_neBot_iff : NeBotNeBot (Filter.cocompact X) ↔ NoncompactSpace X :=
  ⟨noncompactSpace_of_neBot, fun _ => inferInstance⟩

Nontriviality of Cocompact Filter $\leftrightarrow$ Noncompact Space

Informal description

The cocompact filter on a topological space $X$ is nontrivial if and only if $X$ is a noncompact space.

not_compactSpace_iff theorem

: ¬CompactSpace X ↔ NoncompactSpace X

Full source

theorem not_compactSpace_iff : ¬CompactSpace X¬CompactSpace X ↔ NoncompactSpace X :=
  ⟨fun h₁ => ⟨fun h₂ => h₁ ⟨h₂⟩⟩, fun ⟨h₁⟩ ⟨h₂⟩ => h₁ h₂⟩

Equivalence of Non-Compactness and Noncompact Space

Informal description

A topological space $X$ is not compact if and only if it is noncompact.

instNoncompactSpaceInt instance

: NoncompactSpace ℤ

Full source

instance : NoncompactSpace ℤ :=
  noncompactSpace_of_neBot <| by simp only [Filter.cocompact_eq_cofinite, Filter.cofinite_neBot]

Noncompactness of the Integers

Informal description

The integers $\mathbb{Z}$ form a noncompact space.

finite_of_compact_of_discrete theorem

[CompactSpace X] [DiscreteTopology X] : Finite X

Full source

/-- A compact discrete space is finite. -/
theorem finite_of_compact_of_discrete [CompactSpace X] [DiscreteTopology X] : Finite X :=
  Finite.of_finite_univ <| isCompact_univ.finite_of_discrete

Compact Discrete Spaces are Finite

Informal description

If a topological space $X$ is both compact and has the discrete topology, then $X$ is finite.

Set.Infinite.exists_accPt_cofinite_inf_principal_of_subset_isCompact theorem

{K : Set X} (hs : s.Infinite) (hK : IsCompact K) (hsub : s ⊆ K) : ∃ x ∈ K, AccPt x (cofinite ⊓ 𝓟 s)

Full source

lemma Set.Infinite.exists_accPt_cofinite_inf_principal_of_subset_isCompact
    {K : Set X} (hs : s.Infinite) (hK : IsCompact K) (hsub : s ⊆ K) :
    ∃ x ∈ K, AccPt x (cofinite ⊓ 𝓟 s) :=
  (@hK _ hs.cofinite_inf_principal_neBot (inf_le_right.trans <| principal_mono.2 hsub)).imp
    fun x hx ↦ by rwa [accPt_iff_clusterPt, inf_comm, inf_right_comm,
      (finite_singleton _).cofinite_inf_principal_compl]

Existence of Accumulation Point for Infinite Subset of Compact Set with Cofinite Filter

Informal description

Let $X$ be a topological space, $K \subseteq X$ a compact subset, and $s \subseteq K$ an infinite subset. Then there exists a point $x \in K$ that is an accumulation point of $s$ with respect to the filter $\text{cofinite} \cap \mathcal{P}(s)$.

Set.Infinite.exists_accPt_of_subset_isCompact theorem

{K : Set X} (hs : s.Infinite) (hK : IsCompact K) (hsub : s ⊆ K) : ∃ x ∈ K, AccPt x (𝓟 s)

Full source

lemma Set.Infinite.exists_accPt_of_subset_isCompact {K : Set X} (hs : s.Infinite)
    (hK : IsCompact K) (hsub : s ⊆ K) : ∃ x ∈ K, AccPt x (𝓟 s) :=
  let ⟨x, hxK, hx⟩ := hs.exists_accPt_cofinite_inf_principal_of_subset_isCompact hK hsub
  ⟨x, hxK, hx.mono inf_le_right⟩

Existence of Accumulation Point for Infinite Subset of Compact Set

Informal description

Let $X$ be a topological space, $K \subseteq X$ a compact subset, and $s \subseteq K$ an infinite subset. Then there exists a point $x \in K$ that is an accumulation point of $s$ with respect to the principal filter generated by $s$.

Set.Infinite.exists_accPt_cofinite_inf_principal theorem

[CompactSpace X] (hs : s.Infinite) : ∃ x, AccPt x (cofinite ⊓ 𝓟 s)

Full source

lemma Set.Infinite.exists_accPt_cofinite_inf_principal [CompactSpace X] (hs : s.Infinite) :
    ∃ x, AccPt x (cofinite ⊓ 𝓟 s) := by
  simpa only [mem_univ, true_and]
    using hs.exists_accPt_cofinite_inf_principal_of_subset_isCompact isCompact_univ s.subset_univ

Existence of Accumulation Point for Infinite Subset in Compact Space with Cofinite Filter

Informal description

Let $X$ be a compact space and $s \subseteq X$ an infinite subset. Then there exists a point $x \in X$ that is an accumulation point of $s$ with respect to the filter $\text{cofinite} \cap \mathcal{P}(s)$.

Set.Infinite.exists_accPt_principal theorem

[CompactSpace X] (hs : s.Infinite) : ∃ x, AccPt x (𝓟 s)

Full source

lemma Set.Infinite.exists_accPt_principal [CompactSpace X] (hs : s.Infinite) : ∃ x, AccPt x (𝓟 s) :=
  hs.exists_accPt_cofinite_inf_principal.imp fun _x hx ↦ hx.mono inf_le_right

Existence of Accumulation Point for Infinite Subset in Compact Space

Informal description

Let $X$ be a compact space and $s \subseteq X$ an infinite subset. Then there exists a point $x \in X$ that is an accumulation point of $s$ with respect to the principal filter generated by $s$.

exists_nhds_ne_neBot theorem

(X : Type*) [TopologicalSpace X] [CompactSpace X] [Infinite X] : ∃ z : X, (𝓝[≠] z).NeBot

Full source

theorem exists_nhds_ne_neBot (X : Type*) [TopologicalSpace X] [CompactSpace X] [Infinite X] :
    ∃ z : X, (𝓝[≠] z).NeBot := by
  simpa [AccPt] using (@infinite_univ X _).exists_accPt_principal

Existence of Non-Trivial Punctured Neighborhood in Infinite Compact Space

Informal description

Let $X$ be an infinite compact topological space. Then there exists a point $z \in X$ such that the punctured neighborhood filter $\mathcal{N}_z \setminus \{z\}$ is non-trivial (i.e., contains a non-empty set).

finite_cover_nhds_interior theorem

[CompactSpace X] {U : X → Set X} (hU : ∀ x, U x ∈ 𝓝 x) : ∃ t : Finset X, ⋃ x ∈ t, interior (U x) = univ

Full source

theorem finite_cover_nhds_interior [CompactSpace X] {U : X → Set X} (hU : ∀ x, U x ∈ 𝓝 x) :
    ∃ t : Finset X, ⋃ x ∈ t, interior (U x) = univ :=
  let ⟨t, ht⟩ := isCompact_univ.elim_finite_subcover (fun x => interior (U x))
    (fun _ => isOpen_interior) fun x _ => mem_iUnion.2 ⟨x, mem_interior_iff_mem_nhds.2 (hU x)⟩
  ⟨t, univ_subset_iff.1 ht⟩

Finite Interior Cover of Compact Space by Neighborhoods

Informal description

Let $X$ be a compact space and $\{U(x)\}_{x \in X}$ a family of neighborhoods of each point $x \in X$ (i.e., $U(x) \in \mathcal{N}_x$ for each $x$). Then there exists a finite subset $t \subseteq X$ such that the union of the interiors of $U(x)$ for $x \in t$ covers $X$, i.e., $\bigcup_{x \in t} \text{interior}(U(x)) = \text{univ}$.

finite_cover_nhds theorem

[CompactSpace X] {U : X → Set X} (hU : ∀ x, U x ∈ 𝓝 x) : ∃ t : Finset X, ⋃ x ∈ t, U x = univ

Full source

theorem finite_cover_nhds [CompactSpace X] {U : X → Set X} (hU : ∀ x, U x ∈ 𝓝 x) :
    ∃ t : Finset X, ⋃ x ∈ t, U x = univ :=
  let ⟨t, ht⟩ := finite_cover_nhds_interior hU
  ⟨t, univ_subset_iff.1 <| ht.symm.subset.trans <| iUnion₂_mono fun _ _ => interior_subset⟩

Finite Cover of Compact Space by Neighborhoods

Informal description

Let $X$ be a compact space and $\{U(x)\}_{x \in X}$ a family of neighborhoods of each point $x \in X$ (i.e., $U(x)$ is a neighborhood of $x$ for each $x$). Then there exists a finite subset $t \subseteq X$ such that the union of $U(x)$ for $x \in t$ covers $X$, i.e., $\bigcup_{x \in t} U(x) = X$.

Filter.comap_cocompact_le theorem

{f : X → Y} (hf : Continuous f) : (Filter.cocompact Y).comap f ≤ Filter.cocompact X

Full source

/-- 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 Filter.comap_cocompact_le {f : X → Y} (hf : Continuous f) :
    (Filter.cocompact Y).comap f ≤ Filter.cocompact X := by
  rw [(Filter.hasBasis_cocompact.comap f).le_basis_iff Filter.hasBasis_cocompact]
  intro t ht
  refine ⟨f '' t, ht.image hf, ?_⟩
  simpa using t.subset_preimage_image f

Preimage of Cocompact Filter Under Continuous Function is Contained in Cocompact Filter

Informal description

Let $X$ and $Y$ be topological spaces and $f \colon X \to Y$ a continuous function. Then the preimage filter of the cocompact filter on $Y$ under $f$ is contained in the cocompact filter on $X$. In other words, for any set $s \subseteq Y$ whose complement is compact, the preimage $f^{-1}(s)$ has a compact complement in $X$.

disjoint_map_cocompact theorem

 {g : X → Y} {f : Filter X} (hg : Continuous g) (hf : Disjoint f (Filter.cocompact X)) :
  Disjoint (map g f) (Filter.cocompact Y)

Full source

/-- If a filter is disjoint from the cocompact filter, so is its image under any continuous
function. -/
theorem disjoint_map_cocompact {g : X → Y} {f : Filter X} (hg : Continuous g)
    (hf : Disjoint f (Filter.cocompact X)) : Disjoint (map g f) (Filter.cocompact Y) := by
  rw [← Filter.disjoint_comap_iff_map, disjoint_iff_inf_le]
  calc
    f ⊓ (comap g (cocompact Y))
    _ ≤ f ⊓ Filter.cocompact X := inf_le_inf_left f (Filter.comap_cocompact_le hg)
    _ = ⊥ := disjoint_iff.mp hf

Disjointness of Image Filter and Cocompact Filter under Continuous Maps

Informal description

Let $X$ and $Y$ be topological spaces, $g \colon X \to Y$ a continuous function, and $f$ a filter on $X$ that is disjoint from the cocompact filter on $X$. Then the image filter $\operatorname{map} g f$ is disjoint from the cocompact filter on $Y$.

isCompact_range theorem

[CompactSpace X] {f : X → Y} (hf : Continuous f) : IsCompact (range f)

Full source

theorem isCompact_range [CompactSpace X] {f : X → Y} (hf : Continuous f) : IsCompact (range f) := by
  rw [← image_univ]; exact isCompact_univ.image hf

Range of a Continuous Function from a Compact Space is Compact

Informal description

If $X$ is a compact space and $f \colon X \to Y$ is a continuous function, then the range of $f$ is a compact subset of $Y$.

isCompact_diagonal theorem

[CompactSpace X] : IsCompact (diagonal X)

Full source

theorem isCompact_diagonal [CompactSpace X] : IsCompact (diagonal X) :=
  @range_diag X ▸ isCompact_range (continuous_id.prodMk continuous_id)

Compactness of the Diagonal in a Compact Space

Informal description

If $X$ is a compact space, then the diagonal $\Delta_X = \{(x, x) \mid x \in X\}$ is a compact subset of $X \times X$.

isClosedMap_snd_of_compactSpace theorem

[CompactSpace X] : IsClosedMap (Prod.snd : X × Y → Y)

Full source

/-- If `X` is a compact topological space, then `Prod.snd : X × Y → Y` is a closed map. -/
theorem isClosedMap_snd_of_compactSpace [CompactSpace X] :
    IsClosedMap (Prod.snd : X × Y → Y) := fun s hs => by
  rw [← isOpen_compl_iff, isOpen_iff_mem_nhds]
  intro y hy
  have : univuniv ×ˢ {y} ⊆ sᶜ := by
    exact fun (x, y') ⟨_, rfl⟩ hs => hy ⟨(x, y'), hs, rfl⟩
  rcases generalized_tube_lemma isCompact_univ isCompact_singleton hs.isOpen_compl this
    with ⟨U, V, -, hVo, hU, hV, hs⟩
  refine mem_nhds_iff.2 ⟨V, ?_, hVo, hV rfl⟩
  rintro _ hzV ⟨z, hzs, rfl⟩
  exact hs ⟨hU trivial, hzV⟩ hzs

Projection to Second Factor is Closed Map for Compact First Factor

Informal description

If $X$ is a compact topological space, then the projection map $\operatorname{snd} \colon X \times Y \to Y$ is a closed map, meaning it sends closed subsets of $X \times Y$ to closed subsets of $Y$.

isClosedMap_fst_of_compactSpace theorem

[CompactSpace Y] : IsClosedMap (Prod.fst : X × Y → X)

Full source

/-- If `Y` is a compact topological space, then `Prod.fst : X × Y → X` is a closed map. -/
theorem isClosedMap_fst_of_compactSpace [CompactSpace Y] : IsClosedMap (Prod.fst : X × Y → X) :=
  isClosedMap_snd_of_compactSpace.comp isClosedMap_swap

Projection to First Factor is Closed Map for Compact Second Factor

Informal description

If $Y$ is a compact topological space, then the projection map $\operatorname{fst} \colon X \times Y \to X$ is a closed map, meaning it sends closed subsets of $X \times Y$ to closed subsets of $X$.

exists_subset_nhds_of_compactSpace theorem

 [CompactSpace X] [Nonempty ι] {V : ι → Set X} (hV : Directed (· ⊇ ·) V) (hV_closed : ∀ i, IsClosed (V i)) {U : Set X}
  (hU : ∀ x ∈ ⋂ i, V i, U ∈ 𝓝 x) : ∃ i, V i ⊆ U

Full source

theorem exists_subset_nhds_of_compactSpace [CompactSpace X] [Nonempty ι]
    {V : ι → Set X} (hV : Directed (· ⊇ ·) V) (hV_closed : ∀ i, IsClosed (V i)) {U : Set X}
    (hU : ∀ x ∈ ⋂ i, V i, U ∈ 𝓝 x) : ∃ i, V i ⊆ U :=
  exists_subset_nhds_of_isCompact' hV (fun i => (hV_closed i).isCompact) hV_closed hU

Neighborhood Containment Property for Directed Families of Closed Sets in Compact Spaces

Informal description

Let $X$ be a compact topological space and $\{V_i\}_{i \in \iota}$ a nonempty directed family of closed subsets of $X$ with respect to reverse inclusion ($\supseteq$). If $U$ is a neighborhood of the intersection $\bigcap_{i \in \iota} V_i$ (i.e., for every $x \in \bigcap_{i \in \iota} V_i$, $U$ contains an open neighborhood of $x$), then there exists some index $i$ such that $V_i \subseteq U$.

Topology.IsInducing.isCompact_iff theorem

{f : X → Y} (hf : IsInducing f) : IsCompact s ↔ IsCompact (f '' s)

Full source

/-- If `f : X → Y` is an inducing map, the image `f '' s` of a set `s` is compact
  if and only if `s` is compact. -/
theorem Topology.IsInducing.isCompact_iff {f : X → Y} (hf : IsInducing f) :
    IsCompactIsCompact s ↔ IsCompact (f '' s) := by
  refine ⟨fun hs => hs.image hf.continuous, fun hs F F_ne_bot F_le => ?_⟩
  obtain ⟨_, ⟨x, x_in : x ∈ s, rfl⟩, hx : ClusterPt (f x) (map f F)⟩ :=
    hs ((map_mono F_le).trans_eq map_principal)
  exact ⟨x, x_in, hf.mapClusterPt_iff.1 hx⟩

Compactness under Inducing Maps: $s$ Compact $\iff$ $f(s)$ Compact

Informal description

Let $X$ and $Y$ be topological spaces, $f : X \to Y$ an inducing map, and $s \subseteq X$ a subset. Then $s$ is compact if and only if its image $f(s)$ is compact in $Y$.

Topology.IsEmbedding.isCompact_iff theorem

{f : X → Y} (hf : IsEmbedding f) : IsCompact s ↔ IsCompact (f '' s)

Full source

/-- If `f : X → Y` is an embedding, the image `f '' s` of a set `s` is compact
if and only if `s` is compact. -/
theorem Topology.IsEmbedding.isCompact_iff {f : X → Y} (hf : IsEmbedding f) :
    IsCompactIsCompact s ↔ IsCompact (f '' s) := hf.isInducing.isCompact_iff

Compactness under Embeddings: $s$ Compact $\iff$ $f(s)$ Compact

Informal description

Let $X$ and $Y$ be topological spaces, $f : X \to Y$ be an embedding, and $s \subseteq X$ a subset. Then $s$ is compact if and only if its image $f(s)$ is compact in $Y$.

Topology.IsInducing.isCompact_preimage theorem

(hf : IsInducing f) (hf' : IsClosed (range f)) {K : Set Y} (hK : IsCompact K) : IsCompact (f ⁻¹' K)

Full source

/-- The preimage of a compact set under an inducing map is a compact set. -/
theorem Topology.IsInducing.isCompact_preimage (hf : IsInducing f) (hf' : IsClosed (range f))
    {K : Set Y} (hK : IsCompact K) : IsCompact (f ⁻¹' K) := by
  replace hK := hK.inter_right hf'
  rwa [hf.isCompact_iff, image_preimage_eq_inter_range]

Compactness of Preimage under Inducing Map with Closed Range

Informal description

Let $X$ and $Y$ be topological spaces, $f : X \to Y$ an inducing map with closed range, and $K \subseteq Y$ a compact set. Then the preimage $f^{-1}(K)$ is compact in $X$.

Topology.IsInducing.isCompact_preimage_iff theorem

{f : X → Y} (hf : IsInducing f) {K : Set Y} (Kf : K ⊆ range f) : IsCompact (f ⁻¹' K) ↔ IsCompact K

Full source

lemma Topology.IsInducing.isCompact_preimage_iff {f : X → Y} (hf : IsInducing f) {K : Set Y}
    (Kf : K ⊆ range f) : IsCompactIsCompact (f ⁻¹' K) ↔ IsCompact K := by
  rw [hf.isCompact_iff, image_preimage_eq_of_subset Kf]

Compactness of Preimage under Inducing Map: $f^{-1}(K)$ Compact $\iff$ $K$ Compact

Informal description

Let $X$ and $Y$ be topological spaces, $f : X \to Y$ an inducing map, and $K \subseteq Y$ a subset contained in the range of $f$. Then the preimage $f^{-1}(K)$ is compact in $X$ if and only if $K$ is compact in $Y$.

Topology.IsInducing.isCompact_preimage' theorem

(hf : IsInducing f) {K : Set Y} (hK : IsCompact K) (Kf : K ⊆ range f) : IsCompact (f ⁻¹' K)

Full source

/-- The preimage of a compact set in the image of an inducing map is compact. -/
lemma Topology.IsInducing.isCompact_preimage' (hf : IsInducing f) {K : Set Y}
    (hK : IsCompact K) (Kf : K ⊆ range f) : IsCompact (f ⁻¹' K) :=
  (hf.isCompact_preimage_iff Kf).2 hK

Compactness of Preimage under Inducing Map with Range Condition

Informal description

Let $X$ and $Y$ be topological spaces, $f : X \to Y$ an inducing map, and $K \subseteq Y$ a compact subset contained in the range of $f$. Then the preimage $f^{-1}(K)$ is compact in $X$.

Topology.IsClosedEmbedding.isCompact_preimage theorem

(hf : IsClosedEmbedding f) {K : Set Y} (hK : IsCompact K) : IsCompact (f ⁻¹' K)

Full source

/-- The preimage of a compact set under a closed embedding is a compact set. -/
theorem Topology.IsClosedEmbedding.isCompact_preimage (hf : IsClosedEmbedding f)
    {K : Set Y} (hK : IsCompact K) : IsCompact (f ⁻¹' K) :=
  hf.isInducing.isCompact_preimage (hf.isClosed_range) hK

Compactness of Preimage under Closed Embedding

Informal description

Let $X$ and $Y$ be topological spaces, $f : X \to Y$ a closed embedding, and $K \subseteq Y$ a compact set. Then the preimage $f^{-1}(K)$ is compact in $X$.

Topology.IsClosedEmbedding.tendsto_cocompact theorem

(hf : IsClosedEmbedding f) : Tendsto f (Filter.cocompact X) (Filter.cocompact Y)

Full source

/-- 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 `IsClosedEmbedding.isCompact_preimage`. -/
theorem Topology.IsClosedEmbedding.tendsto_cocompact (hf : IsClosedEmbedding f) :
    Tendsto f (Filter.cocompact X) (Filter.cocompact Y) :=
  Filter.hasBasis_cocompact.tendsto_right_iff.mpr fun _K hK =>
    (hf.isCompact_preimage hK).compl_mem_cocompact

Closed embeddings preserve cocompactness

Informal description

Let $X$ and $Y$ be topological spaces and $f : X \to Y$ be a closed embedding. Then $f$ maps cocompact sets in $X$ to cocompact sets in $Y$, i.e., the image of any cocompact filter on $X$ under $f$ is contained in the cocompact filter on $Y$.

Subtype.isCompact_iff theorem

{p : X → Prop} {s : Set { x // p x }} : IsCompact s ↔ IsCompact ((↑) '' s : Set X)

Full source

/-- Sets of subtype are compact iff the image under a coercion is. -/
theorem Subtype.isCompact_iff {p : X → Prop} {s : Set { x // p x }} :
    IsCompactIsCompact s ↔ IsCompact ((↑) '' s : Set X) :=
  IsEmbedding.subtypeVal.isCompact_iff

Compactness of Subtype Sets via Coercion Image

Informal description

Let $X$ be a topological space and $p : X \to \mathrm{Prop}$ be a predicate on $X$. For any subset $s$ of the subtype $\{x \in X \mid p(x)\}$, $s$ is compact if and only if its image under the canonical inclusion map (i.e., the coercion $\uparrow$) is compact in $X$.

isCompact_iff_isCompact_univ theorem

: IsCompact s ↔ IsCompact (univ : Set s)

Full source

theorem isCompact_iff_isCompact_univ : IsCompactIsCompact s ↔ IsCompact (univ : Set s) := by
  rw [Subtype.isCompact_iff, image_univ, Subtype.range_coe]

Compactness of Subset vs. Compactness of Subtype Universe

Informal description

A subset $s$ of a topological space is compact if and only if the entire space of the subtype corresponding to $s$ (i.e., the set $\text{univ} : \text{Set } s$) is compact.

isCompact_iff_compactSpace theorem

: IsCompact s ↔ CompactSpace s

Full source

theorem isCompact_iff_compactSpace : IsCompactIsCompact s ↔ CompactSpace s :=
  isCompact_iff_isCompact_univ.trans isCompact_univ_iff

Compactness of Subset Equivalence to Compact Space Property

Informal description

A subset $s$ of a topological space is compact if and only if the subspace $s$ equipped with the subspace topology is a compact space.

IsCompact.finite theorem

(hs : IsCompact s) (hs' : DiscreteTopology s) : s.Finite

Full source

theorem IsCompact.finite (hs : IsCompact s) (hs' : DiscreteTopology s) : s.Finite :=
  finite_coe_iff.mp (@finite_of_compact_of_discrete _ _ (isCompact_iff_compactSpace.mp hs) hs')

Compact Discrete Subsets are Finite

Informal description

If a subset $s$ of a topological space is compact and has the discrete topology, then $s$ is finite.

exists_nhds_ne_inf_principal_neBot theorem

(hs : IsCompact s) (hs' : s.Infinite) : ∃ z ∈ s, (𝓝[≠] z ⊓ 𝓟 s).NeBot

Full source

theorem exists_nhds_ne_inf_principal_neBot (hs : IsCompact s) (hs' : s.Infinite) :
    ∃ z ∈ s, (𝓝[≠] z ⊓ 𝓟 s).NeBot :=
  hs'.exists_accPt_of_subset_isCompact hs Subset.rfl

Existence of Non-Trivial Punctured Neighborhood Intersection for Infinite Compact Sets

Informal description

Let $X$ be a topological space and $s \subseteq X$ an infinite subset that is compact. Then there exists a point $z \in s$ such that the intersection of the punctured neighborhood filter of $z$ and the principal filter generated by $s$ is non-trivial (i.e., contains more than just the empty set).

Topology.IsClosedEmbedding.noncompactSpace theorem

[NoncompactSpace X] {f : X → Y} (hf : IsClosedEmbedding f) : NoncompactSpace Y

Full source

protected theorem Topology.IsClosedEmbedding.noncompactSpace [NoncompactSpace X] {f : X → Y}
    (hf : IsClosedEmbedding f) : NoncompactSpace Y :=
  noncompactSpace_of_neBot hf.tendsto_cocompact.neBot

Noncompactness under Closed Embeddings: $X$ Noncompact $\Rightarrow$ $Y$ Noncompact

Informal description

Let $X$ and $Y$ be topological spaces, and let $f : X \to Y$ be a closed embedding. If $X$ is noncompact, then $Y$ is noncompact.

Topology.IsClosedEmbedding.compactSpace theorem

[h : CompactSpace Y] {f : X → Y} (hf : IsClosedEmbedding f) : CompactSpace X

Full source

protected theorem Topology.IsClosedEmbedding.compactSpace [h : CompactSpace Y] {f : X → Y}
    (hf : IsClosedEmbedding f) : CompactSpace X :=
  ⟨by rw [hf.isInducing.isCompact_iff, image_univ]; exact hf.isClosed_range.isCompact⟩

Compactness under Closed Embeddings: $Y$ Compact $\Rightarrow$ $X$ Compact

Informal description

Let $X$ and $Y$ be topological spaces, and let $f : X \to Y$ be a closed embedding. If $Y$ is compact, then $X$ is compact.

IsCompact.prod theorem

{t : Set Y} (hs : IsCompact s) (ht : IsCompact t) : IsCompact (s ×ˢ t)

Full source

theorem IsCompact.prod {t : Set Y} (hs : IsCompact s) (ht : IsCompact t) :
    IsCompact (s ×ˢ t) := by
  rw [isCompact_iff_ultrafilter_le_nhds'] at hs ht ⊢
  intro f hfs
  obtain ⟨x : X, sx : x ∈ s, hx : map Prod.fst f.1 ≤ 𝓝 x⟩ :=
    hs (f.map Prod.fst) (mem_map.2 <| mem_of_superset hfs fun x => And.left)
  obtain ⟨y : Y, ty : y ∈ t, hy : map Prod.snd f.1 ≤ 𝓝 y⟩ :=
    ht (f.map Prod.snd) (mem_map.2 <| mem_of_superset hfs fun x => And.right)
  rw [map_le_iff_le_comap] at hx hy
  refine ⟨⟨x, y⟩, ⟨sx, ty⟩, ?_⟩
  rw [nhds_prod_eq]; exact le_inf hx hy

Compactness of Cartesian Product of Compact Sets

Informal description

For any topological spaces $X$ and $Y$, if $s \subseteq X$ and $t \subseteq Y$ are compact subsets, then their Cartesian product $s \times t$ is a compact subset of $X \times Y$.

Finite.compactSpace instance

[Finite X] : CompactSpace X

Full source

/-- Finite topological spaces are compact. -/
instance (priority := 100) Finite.compactSpace [Finite X] : CompactSpace X where
  isCompact_univ := finite_univ.isCompact

Finite Spaces are Compact

Informal description

Every finite topological space is compact.

ULift.compactSpace instance

[CompactSpace X] : CompactSpace (ULift.{v} X)

Full source

instance ULift.compactSpace [CompactSpace X] : CompactSpace (ULift.{v} X) :=
  IsClosedEmbedding.uliftDown.compactSpace

Compactness of Lifted Spaces

Informal description

For any compact topological space $X$, the lifted space $\mathrm{ULift}\, X$ is also compact.

instCompactSpaceProd instance

[CompactSpace X] [CompactSpace Y] : CompactSpace (X × Y)

Full source

/-- The product of two compact spaces is compact. -/
instance [CompactSpace X] [CompactSpace Y] : CompactSpace (X × Y) :=
  ⟨by rw [← univ_prod_univ]; exact isCompact_univ.prod isCompact_univ⟩

Compactness of Product Spaces

Informal description

The product $X \times Y$ of two compact spaces $X$ and $Y$ is compact.

instCompactSpaceSum instance

[CompactSpace X] [CompactSpace Y] : CompactSpace (X ⊕ Y)

Full source

/-- The disjoint union of two compact spaces is compact. -/
instance [CompactSpace X] [CompactSpace Y] : CompactSpace (X ⊕ Y) :=
  ⟨by
    rw [← range_inl_union_range_inr]
    exact (isCompact_range continuous_inl).union (isCompact_range continuous_inr)⟩

Compactness of Disjoint Union of Compact Spaces

Informal description

The disjoint union $X \oplus Y$ of two compact spaces $X$ and $Y$ is compact.

instCompactSpaceSigmaOfFinite instance

{X : ι → Type*} [Finite ι] [∀ i, TopologicalSpace (X i)] [∀ i, CompactSpace (X i)] : CompactSpace (Σ i, X i)

Full source

instance {X : ι → Type*} [Finite ι] [∀ i, TopologicalSpace (X i)] [∀ i, CompactSpace (X i)] :
    CompactSpace (Σi, X i) := by
  refine ⟨?_⟩
  rw [Sigma.univ]
  exact isCompact_iUnion fun i => isCompact_range continuous_sigmaMk

Compactness of Finite Disjoint Union of Compact Spaces

Informal description

For a finite index set $\iota$ and a family of topological spaces $\{X_i\}_{i \in \iota}$ where each $X_i$ is compact, the disjoint union $\Sigma i, X_i$ is also compact.

Filter.coprod_cocompact theorem

: (Filter.cocompact X).coprod (Filter.cocompact Y) = Filter.cocompact (X × Y)

Full source

/-- The coproduct of the cocompact filters on two topological spaces is the cocompact filter on
their product. -/
theorem Filter.coprod_cocompact :
    (Filter.cocompact X).coprod (Filter.cocompact Y) = Filter.cocompact (X × Y) := by
  apply le_antisymm
  · exact sup_le (comap_cocompact_le continuous_fst) (comap_cocompact_le continuous_snd)
  · refine (hasBasis_cocompact.coprod hasBasis_cocompact).ge_iff.2 fun K hK ↦ ?_
    rw [← univ_prod, ← prod_univ, ← compl_prod_eq_union]
    exact (hK.1.prod hK.2).compl_mem_cocompact

Coproduct of Cocompact Filters Equals Cocompact Filter of Product Space

Informal description

The coproduct of the cocompact filters on two topological spaces $X$ and $Y$ is equal to the cocompact filter on their product space $X \times Y$.

Prod.noncompactSpace_iff theorem

: NoncompactSpace (X × Y) ↔ NoncompactSpace X ∧ Nonempty Y ∨ Nonempty X ∧ NoncompactSpace Y

Full source

theorem Prod.noncompactSpace_iff :
    NoncompactSpaceNoncompactSpace (X × Y) ↔ NoncompactSpace X ∧ Nonempty Y ∨ Nonempty X ∧ NoncompactSpace Y := by
  simp [← Filter.cocompact_neBot_iff, ← Filter.coprod_cocompact, Filter.coprod_neBot_iff]

Characterization of Noncompactness in Product Spaces

Informal description

The product space $X \times Y$ is noncompact if and only if either $X$ is noncompact and $Y$ is nonempty, or $X$ is nonempty and $Y$ is noncompact.

Prod.noncompactSpace_left instance

[NoncompactSpace X] [Nonempty Y] : NoncompactSpace (X × Y)

Full source

instance (priority := 100) Prod.noncompactSpace_left [NoncompactSpace X] [Nonempty Y] :
    NoncompactSpace (X × Y) :=
  Prod.noncompactSpace_iff.2 (Or.inl ⟨‹_›, ‹_›⟩)

Noncompactness of Product Space (Left Factor)

Informal description

For any noncompact space $X$ and nonempty space $Y$, the product space $X \times Y$ is noncompact.

Prod.noncompactSpace_right instance

[Nonempty X] [NoncompactSpace Y] : NoncompactSpace (X × Y)

Full source

instance (priority := 100) Prod.noncompactSpace_right [Nonempty X] [NoncompactSpace Y] :
    NoncompactSpace (X × Y) :=
  Prod.noncompactSpace_iff.2 (Or.inr ⟨‹_›, ‹_›⟩)

Noncompactness of Product Space with Noncompact Right Factor

Informal description

For any nonempty space $X$ and noncompact space $Y$, the product space $X \times Y$ is noncompact.

isCompact_pi_infinite theorem

{s : ∀ i, Set (X i)} : (∀ i, IsCompact (s i)) → IsCompact {x : ∀ i, X i | ∀ i, x i ∈ s i}

Full source

/-- **Tychonoff's theorem**: product of compact sets is compact. -/
theorem isCompact_pi_infinite {s : ∀ i, Set (X i)} :
    (∀ i, IsCompact (s i)) → IsCompact { x : ∀ i, X i | ∀ i, x i ∈ s i } := by
  simp only [isCompact_iff_ultrafilter_le_nhds, nhds_pi, le_pi, le_principal_iff]
  intro h f hfs
  have : ∀ i : ι, ∃ x, x ∈ s i ∧ Tendsto (Function.eval i) f (𝓝 x) := by
    refine fun i => h i (f.map _) (mem_map.2 ?_)
    exact mem_of_superset hfs fun x hx => hx i
  choose x hx using this
  exact ⟨x, fun i => (hx i).left, fun i => (hx i).right⟩

Tychonoff's Theorem for Infinite Product of Compact Sets

Informal description

For any family of sets $\{s_i\}_{i \in I}$ where each $s_i$ is a compact subset of $X_i$, the product set $\prod_{i \in I} s_i$ is compact in the product space $\prod_{i \in I} X_i$.

isCompact_univ_pi theorem

{s : ∀ i, Set (X i)} (h : ∀ i, IsCompact (s i)) : IsCompact (pi univ s)

Full source

/-- **Tychonoff's theorem** formulated using `Set.pi`: product of compact sets is compact. -/
theorem isCompact_univ_pi {s : ∀ i, Set (X i)} (h : ∀ i, IsCompact (s i)) :
    IsCompact (pi univ s) := by
  convert isCompact_pi_infinite h
  simp only [← mem_univ_pi, setOf_mem_eq]

Tychonoff's Theorem: Compactness of Product Spaces

Informal description

For any family of sets $\{s_i\}_{i \in I}$ where each $s_i$ is a compact subset of $X_i$, the product set $\prod_{i \in I} s_i$ is compact in the product space $\prod_{i \in I} X_i$.

Pi.compactSpace instance

[∀ i, CompactSpace (X i)] : CompactSpace (∀ i, X i)

Full source

instance Pi.compactSpace [∀ i, CompactSpace (X i)] : CompactSpace (∀ i, X i) :=
  ⟨by rw [← pi_univ univ]; exact isCompact_univ_pi fun i => isCompact_univ⟩

Tychonoff's Theorem: Compactness of Product Spaces

Informal description

For any family of topological spaces $\{X_i\}_{i \in I}$ where each $X_i$ is a compact space, the product space $\prod_{i \in I} X_i$ is also compact.

Function.compactSpace instance

[CompactSpace Y] : CompactSpace (ι → Y)

Full source

instance Function.compactSpace [CompactSpace Y] : CompactSpace (ι → Y) :=
  Pi.compactSpace

Compactness of Function Spaces from Compact Spaces

Informal description

For any compact space $Y$ and any index type $\iota$, the function space $\iota \to Y$ is compact.

Pi.isCompact_iff_of_isClosed theorem

{s : Set (Π i, X i)} (hs : IsClosed s) : IsCompact s ↔ ∀ i, IsCompact (eval i '' s)

Full source

lemma Pi.isCompact_iff_of_isClosed {s : Set (Π i, X i)} (hs : IsClosed s) :
    IsCompactIsCompact s ↔ ∀ i, IsCompact (eval i '' s) := by
  constructor <;> intro H
  · exact fun i ↦ H.image <| continuous_apply i
  · exact IsCompact.of_isClosed_subset (isCompact_univ_pi H) hs (subset_pi_eval_image univ s)

Compactness Criterion for Closed Subsets of Product Spaces

Informal description

Let $X_i$ be a family of topological spaces indexed by $i \in I$, and let $s$ be a closed subset of the product space $\prod_{i \in I} X_i$. Then $s$ is compact if and only if for every $i \in I$, the projection $\operatorname{eval}_i(s)$ is compact in $X_i$.

Pi.exists_compact_superset_iff theorem

{s : Set (Π i, X i)} : (∃ K, IsCompact K ∧ s ⊆ K) ↔ ∀ i, ∃ Ki, IsCompact Ki ∧ s ⊆ eval i ⁻¹' Ki

Full source

protected lemma Pi.exists_compact_superset_iff {s : Set (Π i, X i)} :
    (∃ K, IsCompact K ∧ s ⊆ K) ↔ ∀ i, ∃ Ki, IsCompact Ki ∧ s ⊆ eval i ⁻¹' Ki := by
  constructor
  · intro ⟨K, hK, hsK⟩ i
    exact ⟨eval i '' K, hK.image <| continuous_apply i, hsK.trans <| K.subset_preimage_image _⟩
  · intro H
    choose K hK hsK using H
    exact ⟨pi univ K, isCompact_univ_pi hK, fun _ hx i _ ↦ hsK i hx⟩

Existence of Compact Supersets in Product Spaces via Componentwise Compactness

Informal description

For any set $s$ in the product space $\prod_{i} X_i$, there exists a compact superset $K$ of $s$ if and only if for every index $i$, there exists a compact set $K_i$ in $X_i$ such that $s$ is contained in the preimage of $K_i$ under the evaluation map at $i$.

Filter.coprodᵢ_cocompact theorem

 {X : ι → Type*} [∀ d, TopologicalSpace (X d)] :
  (Filter.coprodᵢ fun d => Filter.cocompact (X d)) = Filter.cocompact (∀ d, X d)

Full source

/-- **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`. -/
theorem Filter.coprodᵢ_cocompact {X : ι → Type*} [∀ d, TopologicalSpace (X d)] :
    (Filter.coprodᵢ fun d => Filter.cocompact (X d)) = Filter.cocompact (∀ d, X d) := by
  refine le_antisymm (iSup_le fun i => Filter.comap_cocompact_le (continuous_apply i)) ?_
  refine compl_surjective.forall.2 fun s H => ?_
  simp only [compl_mem_coprodᵢ, Filter.mem_cocompact, compl_subset_compl, image_subset_iff] at H ⊢
  choose K hKc htK using H
  exact ⟨Set.pi univ K, isCompact_univ_pi hKc, fun f hf i _ => htK i hf⟩

Tychonoff's Theorem in Terms of Filters: Cocompact Filter Equality for Product Spaces

Informal description

For a family of topological spaces $\{X_d\}_{d \in \iota}$, the coproduct filter of the cocompact filters on each $X_d$ is equal to the cocompact filter on the product space $\prod_{d \in \iota} X_d$.

Quot.compactSpace instance

{r : X → X → Prop} [CompactSpace X] : CompactSpace (Quot r)

Full source

instance Quot.compactSpace {r : X → X → Prop} [CompactSpace X] : CompactSpace (Quot r) :=
  ⟨by
    rw [← range_quot_mk]
    exact isCompact_range continuous_quot_mk⟩

Compactness of Quotient Spaces from Compact Spaces

Informal description

For any equivalence relation $r$ on a compact space $X$, the quotient space $\mathrm{Quot}\, r$ is also compact.

Quotient.compactSpace instance

{s : Setoid X} [CompactSpace X] : CompactSpace (Quotient s)

Full source

instance Quotient.compactSpace {s : Setoid X} [CompactSpace X] : CompactSpace (Quotient s) :=
  Quot.compactSpace

Compactness of Quotient Spaces from Compact Spaces via Setoids

Informal description

For any setoid $s$ on a compact space $X$, the quotient space $\mathrm{Quotient}\, s$ is also compact.

IsClosed.exists_minimal_nonempty_closed_subset theorem

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

Full source

theorem IsClosed.exists_minimal_nonempty_closed_subset [CompactSpace X] {S : Set X}
    (hS : IsClosed S) (hne : S.Nonempty) :
    ∃ V : Set X, V ⊆ S ∧ V.Nonempty ∧ IsClosed V ∧
      ∀ V' : Set X, V' ⊆ V → V'.Nonempty → IsClosed V' → V' = V := by
  let opens := { U : Set X | Sᶜ ⊆ U ∧ IsOpen U ∧ Uᶜ.Nonempty }
  obtain ⟨U, h⟩ :=
    zorn_subset opens fun c hc hz => by
      by_cases hcne : c.Nonempty
      · obtain ⟨U₀, hU₀⟩ := hcne
        haveI : Nonempty { U // U ∈ c } := ⟨⟨U₀, hU₀⟩⟩
        obtain ⟨U₀compl, -, -⟩ := hc hU₀
        use ⋃₀ c
        refine ⟨⟨?_, ?_, ?_⟩, fun U hU _ hx => ⟨U, hU, hx⟩⟩
        · exact fun _ hx => ⟨U₀, hU₀, U₀compl hx⟩
        · exact isOpen_sUnion fun _ h => (hc h).2.1
        · convert_to (⋂ U : { U // U ∈ c }, U.1ᶜ).Nonempty
          · ext
            simp only [not_exists, exists_prop, not_and, Set.mem_iInter, Subtype.forall,
              mem_setOf_eq, mem_compl_iff, mem_sUnion]
          apply IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed
          · rintro ⟨U, hU⟩ ⟨U', hU'⟩
            obtain ⟨V, hVc, hVU, hVU'⟩ := hz.directedOn U hU U' hU'
            exact ⟨⟨V, hVc⟩, Set.compl_subset_compl.mpr hVU, Set.compl_subset_compl.mpr hVU'⟩
          · exact fun U => (hc U.2).2.2
          · exact fun U => (hc U.2).2.1.isClosed_compl.isCompact
          · exact fun U => (hc U.2).2.1.isClosed_compl
      · use Sᶜ
        refine ⟨⟨Set.Subset.refl _, isOpen_compl_iff.mpr hS, ?_⟩, fun U Uc => (hcne ⟨U, Uc⟩).elim⟩
        rw [compl_compl]
        exact hne
  obtain ⟨Uc, Uo, Ucne⟩ := h.prop
  refine ⟨Uᶜ, Set.compl_subset_comm.mp Uc, Ucne, Uo.isClosed_compl, ?_⟩
  intro V' V'sub V'ne V'cls
  have : V'ᶜ = U := by
    refine h.eq_of_ge ⟨?_, isOpen_compl_iff.mpr V'cls, ?_⟩ (subset_compl_comm.2 V'sub)
    · exact Set.Subset.trans Uc (Set.subset_compl_comm.mp V'sub)
    · simp only [compl_compl, V'ne]
  rw [← this, compl_compl]

Existence of Minimal Nonempty Closed Subsets in Compact Spaces

Informal description

Let $X$ be a compact topological space and $S \subseteq X$ a nonempty closed subset. Then there exists a subset $V \subseteq S$ that is nonempty, closed, and minimal with respect to these properties, meaning that any nonempty closed subset $V' \subseteq V$ must satisfy $V' = V$.

Main results