update

Author: CoolRmal

Mathlib/Analysis/LocallyConvex/Separation.lean

@@ -322,7 +322,7 @@ theorem iInter_halfSpaces_eq (hs₁ : Convex ℝ s) (hs₂ : IsClosed s) :
 
 /-- A variant of `iInter_halfSpaces_eq`. If `s` is nonempty, then all the halfspaces are
 nontrivial. -/
-theorem iInter_halfSpaces_const_eq (hs₁ : Convex ℝ s) (hs₂ : IsClosed s) :
+theorem iInter_halfSpaces_eq' (hs₁ : Convex ℝ s) (hs₂ : IsClosed s) :
     ∃ (L : (sᶜ : Set E) → StrongDual 𝕜 E) (c : (sᶜ : Set E) → ℝ),
     ⋂ y, { x | re (L y x) ≤ c y } = s ∧ (s.Nonempty → ∀ y, ∃ x, re (L y x) ≠ 0) := by
   have (y : (sᶜ : Set E)) := geometric_hahn_banach_closed_point (𝕜 := 𝕜) hs₁ hs₂ y.2
@@ -339,18 +339,13 @@ theorem iInter_halfSpaces_const_eq (hs₁ : Convex ℝ s) (hs₂ : IsClosed s) :
 
 /-- A closed convex set with a Lindelöf complement is an intersection of countably many
 halfspaces. -/
-theorem _root_.IsLindelof.iInter_countable_halfSpaces_const_eq (hs₁ : Convex ℝ s) (hs₂ : IsClosed s)
-    (hs₃ : IsLindelof sᶜ) : ∃ (u : Set (sᶜ : Set E)) (L : u → StrongDual 𝕜 E) (c : u → ℝ),
-    u.Countable ∧ ⋂ y, { x | re (L y x) ≤ c y } = s ∧
-    (s.Nonempty → ∀ y, ∃ x, re (L y x) ≠ 0) := by
-  obtain ⟨L, c, hLc⟩ := iInter_halfSpaces_const_eq (𝕜 := 𝕜) hs₁ hs₂
+theorem iInter_countable_halfSpaces_eq [HereditarilyLindelofSpace E] (hs₁ : Convex ℝ s)
+    (hs₂ : IsClosed s) : ∃ L : ℕ → StrongDual 𝕜 E, ∃ c : ℕ → ℝ,
+    ⋂ n, { x | re (L n x) ≤ c n } = s ∧ (s.Nonempty → ∀ y, ∃ x, re (L y x) ≠ 0) := by
+  obtain ⟨L, c, hLc⟩ := iInter_halfSpaces_eq' (𝕜 := 𝕜) hs₁ hs₂
   let t : (sᶜ : Set E) → Set E := fun y => { x | re (L y x) ≤ c y }
-  have htc y : IsClosed (t y) := by
-    suffices t y = re ∘ (L y) ⁻¹' Iic (c y) from by
-      simpa [this] using IsClosed.preimage (by fun_prop) isClosed_Iic
-    grind
-  have hst : sᶜ ∩ ⋂ y, t y = ∅ := by grind
-  obtain ⟨u, hu, hu'⟩ := hs₃.elim_countable_subfamily_closed t htc hst
+  have htc y : IsClosed (t y) := isClosed_le (continuous_re.comp (L y).continuous) continuous_const
+  obtain ⟨u, hu, hu'⟩ := eq_closed_inter_nat t htc
   refine ⟨u, fun y => L y, fun y => c y, hu, subset_antisymm (fun z hz => ?_) ?_, fun h y =>
     hLc.2 h y.1⟩
   · by_contra!
@@ -365,22 +360,6 @@ theorem _root_.IsLindelof.iInter_countable_halfSpaces_const_eq (hs₁ : Convex 
     convert this
     simp
 
-/-- `IsLindelof.iInter_countable_halfSpaces_const_eq` for product spaces. -/
-theorem _root_.IsLindelof.iInter_countable_halfSpaces_const_eq_prod {F : Type*} [AddCommGroup F]
-    [Module ℝ F] [TopologicalSpace F] [Module 𝕜 F] [IsScalarTower ℝ 𝕜 F] [IsTopologicalAddGroup F]
-    [ContinuousSMul 𝕜 F] [LocallyConvexSpace ℝ F] {s : Set (E × F)} (hs₁ : Convex ℝ s)
-    (hs₂ : IsClosed s) (hs₃ : IsLindelof sᶜ) :
-    ∃ (u : Set (sᶜ : Set (E × F))) (L : u → StrongDual 𝕜 E) (T : u → StrongDual 𝕜 F) (c : u → ℝ),
-    u.Countable ∧ ⋂ y, { x | re (L y x.1) + re (T y x.2) ≤ c y } = s
-    ∧ (s.Nonempty → ∀ y, ∃ x z, re (L y x) + re (T y z) ≠ 0):= by
-  obtain ⟨u, LT, c, eq1, eq2⟩ := hs₃.iInter_countable_halfSpaces_const_eq (𝕜 := 𝕜) hs₁ hs₂
-  refine ⟨u, fun i ↦ (LT i).comp (.inl 𝕜 E F), fun i ↦ (LT i).comp (.inr 𝕜 E F), c, eq1, ?_,
-    fun h y => ?_⟩
-  · convert eq2.1
-    simp [← map_add]
-  · obtain ⟨w, hw⟩ := eq2.2 h y
-    simpa [← map_add] using ⟨w.1, w.2, hw⟩
-
 end
 
 end RCLike

Mathlib/Topology/Compactness/Lindelof.lean

@@ -723,13 +723,34 @@ instance (priority := 100) SecondCountableTopology.toHereditarilyLindelof
     use t, htc
     exact subset_of_subset_of_eq hcover (id htu.symm)
 
-lemma eq_open_union_countable [HereditarilyLindelofSpace X] {ι : Type u} (U : ι → Set X)
+lemma eq_open_union_countable [HereditarilyLindelofSpace X] {ι : Type*} (U : ι → Set X)
     (h : ∀ i, IsOpen (U i)) : ∃ t : Set ι, t.Countable ∧ ⋃ i∈t, U i = ⋃ i, U i := by
   have : IsLindelof (⋃ i, U i) := HereditarilyLindelof_LindelofSets (⋃ i, U i)
-  rcases isLindelof_iff_countable_subcover.mp this U h (Eq.subset rfl) with ⟨t, ⟨htc, htu⟩⟩
+  rcases IsLindelof.elim_countable_subcover this U h (Eq.subset rfl) with ⟨t, ⟨htc, htu⟩⟩
   use t, htc
   apply eq_of_subset_of_subset (iUnion₂_subset_iUnion (fun i ↦ i ∈ t) fun i ↦ U i) htu
 
+lemma eq_open_union_nat [HereditarilyLindelofSpace X] {ι : Type*} [Nonempty ι] (U : ι → Set X)
+    (h : ∀ i, IsOpen (U i)) : ∃ k : ℕ → ι, ⋃ n, U (k n) = ⋃ i, U i := by
+  obtain ⟨t, htc, htu⟩ := eq_open_union_countable U h
+  rcases eq_empty_or_nonempty t with rfl | t_ne
+  · simp_rw [mem_empty_iff_false, iUnion_false, iUnion_empty, eq_comm (a := ∅), iUnion_eq_empty]
+      at htu
+    simp [htu]
+  · obtain ⟨k, rfl⟩ := htc.exists_eq_range t_ne
+    use k
+    rwa [biUnion_range] at htu
+
+lemma eq_closed_inter_countable [HereditarilyLindelofSpace X] {ι : Type*} (C : ι → Set X)
+    (h : ∀ i, IsClosed (C i)) : ∃ t : Set ι, t.Countable ∧ ⋂ i∈t, C i = ⋂ i, C i := by
+  conv in _ = _ => rw [← compl_inj_iff]; simp
+  exact eq_open_union_countable (fun i ↦ (C i)ᶜ) (fun i ↦ (h i).isOpen_compl)
+
+lemma eq_closed_inter_nat [HereditarilyLindelofSpace X] {ι : Type*} [Nonempty ι] (C : ι → Set X)
+    (h : ∀ i, IsClosed (C i)) : ∃ k : ℕ → ι, ⋂ n, C (k n) = ⋂ i, C i := by
+  conv in _ = _ => rw [← compl_inj_iff]; simp
+  exact eq_open_union_nat (fun i ↦ (C i)ᶜ) (fun i ↦ (h i).isOpen_compl)
+
 instance HereditarilyLindelof.lindelofSpace_subtype [HereditarilyLindelofSpace X] (p : X → Prop) :
     LindelofSpace {x // p x} := by
   apply isLindelof_iff_LindelofSpace.mp