From b75513bfa194c1cc489acfbe61ea5eed19b6296d Mon Sep 17 00:00:00 2001
From: Anatole Dedecker <anatolededecker@gmail.com>
Date: Fri, 2 Feb 2024 13:15:17 +0000
Subject: [PATCH] feat: add some consequences of Tychonoff's theorem (#10161)

Preliminaries for #6844
The way I prove Ascoli's theorem is by using equicontinuity to reduce it to the case of the product topology, where one can use Tychonoff, hence these variations.
---
 Mathlib/Topology/Compactness/Compact.lean | 17 ++++++++++++++++-
 Mathlib/Topology/Separation.lean          | 12 ++++++++++++
 2 files changed, 28 insertions(+), 1 deletion(-)

diff --git a/Mathlib/Topology/Compactness/Compact.lean b/Mathlib/Topology/Compactness/Compact.lean
index b70b0db42e5c8..5256cf3db8d8d 100644
--- a/Mathlib/Topology/Compactness/Compact.lean
+++ b/Mathlib/Topology/Compactness/Compact.lean
@@ -25,8 +25,8 @@ We define the following properties for sets in a topological space:
 * `isCompact_univ_pi`: **Tychonov's theorem** - an arbitrary product of compact sets
   is compact.
 -/
-open Set Filter Topology TopologicalSpace Classical
 
+open Set Filter Topology TopologicalSpace Classical Function
 
 universe u v
 
@@ -1084,6 +1084,21 @@ instance Function.compactSpace [CompactSpace Y] : CompactSpace (ι → Y) :=
   Pi.compactSpace
 #align function.compact_space Function.compactSpace
 
+lemma Pi.isCompact_iff_of_isClosed {s : Set (Π i, X i)} (hs : IsClosed s) :
+    IsCompact 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)
+
+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⟩
+
 /-- **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)] :
diff --git a/Mathlib/Topology/Separation.lean b/Mathlib/Topology/Separation.lean
index 2b9eec5b511b7..a70718f0a6e9c 100644
--- a/Mathlib/Topology/Separation.lean
+++ b/Mathlib/Topology/Separation.lean
@@ -1675,6 +1675,18 @@ theorem IsCompact.preimage_continuous [CompactSpace X] [T2Space Y] {f : X → Y}
     (hs : IsCompact s) (hf : Continuous f) : IsCompact (f ⁻¹' s) :=
   (hs.isClosed.preimage hf).isCompact
 
+lemma Pi.isCompact_iff {ι : Type*} {π : ι → Type*} [∀ i, TopologicalSpace (π i)]
+    [∀ i, T2Space (π i)] {s : Set (Π i, π i)} :
+    IsCompact s ↔ IsClosed s ∧ ∀ i, IsCompact (eval i '' s):= by
+  constructor <;> intro H
+  · exact ⟨H.isClosed, fun i ↦ H.image <| continuous_apply i⟩
+  · exact IsCompact.of_isClosed_subset (isCompact_univ_pi H.2) H.1 (subset_pi_eval_image univ s)
+
+lemma Pi.isCompact_closure_iff {ι : Type*} {π : ι → Type*} [∀ i, TopologicalSpace (π i)]
+    [∀ i, T2Space (π i)] {s : Set (Π i, π i)} :
+    IsCompact (closure s) ↔ ∀ i, IsCompact (closure <| eval i '' s) := by
+  simp_rw [← exists_isCompact_superset_iff, Pi.exists_compact_superset_iff, image_subset_iff]
+
 /-- If `V : ι → Set X` is a decreasing family of compact sets then any neighborhood of
 `⋂ i, V i` contains some `V i`. This is a version of `exists_subset_nhds_of_isCompact'` where we
 don't need to assume each `V i` closed because it follows from compactness since `X` is