feat: forward-port #18321 (#3101)

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Author: urkud

Mathlib/Data/Analysis/Topology.lean

@@ -4,12 +4,13 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 
 ! This file was ported from Lean 3 source module data.analysis.topology
-! leanprover-community/mathlib commit 28aa996fc6fb4317f0083c4e6daf79878d81be33
+! leanprover-community/mathlib commit 55d771df074d0dd020139ee1cd4b95521422df9f
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
 import Mathlib.Data.Analysis.Filter
 import Mathlib.Topology.Bases
+import Mathlib.Topology.LocallyFinite
 
 /-!
 # Computational realization of topological spaces (experimental)

Mathlib/Topology/Constructions.lean

@@ -4,12 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Mario Carneiro, Patrick Massot
 
 ! This file was ported from Lean 3 source module topology.constructions
-! leanprover-community/mathlib commit 0c1f285a9f6e608ae2bdffa3f993eafb01eba829
+! leanprover-community/mathlib commit 55d771df074d0dd020139ee1cd4b95521422df9f
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
 import Mathlib.Topology.Maps
-import Mathlib.Topology.LocallyFinite
 import Mathlib.Order.Filter.Pi
 
 /-!
@@ -1069,24 +1068,6 @@ theorem tendsto_subtype_rng {β : Type _} {p : α → Prop} {b : Filter β} {f :
   | ⟨a, ha⟩ => by rw [nhds_subtype_eq_comap, tendsto_comap_iff]; rfl
 #align tendsto_subtype_rng tendsto_subtype_rng
 
--- porting note: todo: see https://github.com/leanprover-community/mathlib/pull/18321
-theorem continuous_subtype_nhds_cover {ι : Sort _} {f : α → β} {c : ι → α → Prop}
-    (c_cover : ∀ x : α, ∃ i, { x | c i x } ∈ 𝓝 x)
-    (f_cont : ∀ i, Continuous fun x : Subtype (c i) => f x) : Continuous f :=
-  continuous_iff_continuousAt.mpr fun x => by
-    rcases c_cover x with ⟨i, c_sets⟩
-    lift x to Subtype (c i) using mem_of_mem_nhds c_sets
-    refine' (inducing_subtype_val.continuousAt_iff' _).1 (f_cont i).continuousAt
-    rwa [Subtype.range_coe]
-#align continuous_subtype_nhds_cover continuous_subtype_nhds_cover
-
-/- porting note: todo: see https://github.com/leanprover-community/mathlib/pull/18321
-
-I failed to quickly fix the proof. This is a leaf lemma, and it is going to be replaced by a lemma
-formulated using `ContinuousOn`.
--/
-#noalign continuous_subtype_is_closed_cover
-
 theorem closure_subtype {x : { a // p a }} {s : Set { a // p a }} :
     x ∈ closure s ↔ (x : α) ∈ closure (((↑) : _ → α) '' s) :=
   closure_induced

Mathlib/Topology/ContinuousFunction/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Nicolò Cavalleri
 
 ! This file was ported from Lean 3 source module topology.continuous_function.basic
-! leanprover-community/mathlib commit 6efec6bb9fcaed3cf1baaddb2eaadd8a2a06679c
+! leanprover-community/mathlib commit 55d771df074d0dd020139ee1cd4b95521422df9f
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -365,17 +365,12 @@ variable {ι : Type _} (S : ι → Set α) (φ : ∀ i : ι, C(S i, β))
 /-- A family `φ i` of continuous maps `C(S i, β)`, where the domains `S i` contain a neighbourhood
 of each point in `α` and the functions `φ i` agree pairwise on intersections, can be glued to
 construct a continuous map in `C(α, β)`. -/
-noncomputable def liftCover : C(α, β) := by
-  have H : (⋃ i, S i) = Set.univ := by
-    rw [Set.eq_univ_iff_forall]
-    intro x
-    rw [Set.mem_unionᵢ]
-    obtain ⟨i, hi⟩ := hS x
-    exact ⟨i, mem_of_mem_nhds hi⟩
-  refine' ⟨Set.liftCover S (fun i => φ i) hφ H, continuous_subtype_nhds_cover hS _⟩
-  intro i
-  convert (φ i).continuous
-  apply Set.liftCover_coe
+noncomputable def liftCover : C(α, β) :=
+  haveI H : (⋃ i, S i) = Set.univ :=
+    Set.unionᵢ_eq_univ_iff.2 fun x ↦ (hS x).imp fun _  ↦ mem_of_mem_nhds
+  mk (Set.liftCover S (fun i ↦ φ i) hφ H) <| continuous_of_cover_nhds hS fun i ↦ by
+    rw [continuousOn_iff_continuous_restrict]
+    simpa only [Set.restrict, Set.liftCover_coe] using (φ i).continuous
 #align continuous_map.lift_cover ContinuousMap.liftCover
 
 variable {S φ hφ hS}

Mathlib/Topology/ContinuousOn.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel
 
 ! This file was ported from Lean 3 source module topology.continuous_on
-! leanprover-community/mathlib commit bcfa726826abd57587355b4b5b7e78ad6527b7e4
+! leanprover-community/mathlib commit 55d771df074d0dd020139ee1cd4b95521422df9f
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -227,9 +227,9 @@ theorem nhdsWithin_eq_nhdsWithin {a : α} {s t u : Set α} (h₀ : a ∈ s) (h
   rw [nhdsWithin_restrict t h₀ h₁, nhdsWithin_restrict u h₀ h₁, h₂]
 #align nhds_within_eq_nhds_within nhdsWithin_eq_nhdsWithin
 
--- porting note: new lemma; todo: make it `@[simp]`
-theorem nhdsWithin_eq_nhds {a : α} {s : Set α} : 𝓝[s] a = 𝓝 a ↔ s ∈ 𝓝 a :=
+@[simp] theorem nhdsWithin_eq_nhds {a : α} {s : Set α} : 𝓝[s] a = 𝓝 a ↔ s ∈ 𝓝 a :=
   inf_eq_left.trans le_principal_iff
+#align nhds_within_eq_nhds nhdsWithin_eq_nhds
 
 theorem IsOpen.nhdsWithin_eq {a : α} {s : Set α} (h : IsOpen s) (ha : a ∈ s) : 𝓝[s] a = 𝓝 a :=
   nhdsWithin_eq_nhds.2 <| h.mem_nhds ha
@@ -252,6 +252,22 @@ theorem nhdsWithin_union (a : α) (s t : Set α) : 𝓝[s ∪ t] a = 𝓝[s] a 
   rw [← inf_sup_left, sup_principal]
 #align nhds_within_union nhdsWithin_union
 
+theorem nhdsWithin_bunionᵢ {ι} {I : Set ι} (hI : I.Finite) (s : ι → Set α) (a : α) :
+    𝓝[⋃ i ∈ I, s i] a = ⨆ i ∈ I, 𝓝[s i] a :=
+  Set.Finite.induction_on hI (by simp) fun _ _ hT ↦ by
+    simp only [hT, nhdsWithin_union, supᵢ_insert, bunionᵢ_insert]
+#align nhds_within_bUnion nhdsWithin_bunionᵢ
+
+theorem nhdsWithin_unionₛ {S : Set (Set α)} (hS : S.Finite) (a : α) :
+    𝓝[⋃₀ S] a = ⨆ s ∈ S, 𝓝[s] a := by
+  rw [unionₛ_eq_bunionᵢ, nhdsWithin_bunionᵢ hS]
+#align nhds_within_sUnion nhdsWithin_unionₛ
+
+theorem nhdsWithin_unionᵢ {ι} [Finite ι] (s : ι → Set α) (a : α) :
+    𝓝[⋃ i, s i] a = ⨆ i, 𝓝[s i] a := by
+  rw [← unionₛ_range, nhdsWithin_unionₛ (finite_range s), supᵢ_range]
+#align nhds_within_Union nhdsWithin_unionᵢ
+
 theorem nhdsWithin_inter (a : α) (s t : Set α) : 𝓝[s ∩ t] a = 𝓝[s] a ⊓ 𝓝[t] a := by
   delta nhdsWithin
   rw [inf_left_comm, inf_assoc, inf_principal, ← inf_assoc, inf_idem]
@@ -267,9 +283,9 @@ theorem nhdsWithin_inter_of_mem {a : α} {s t : Set α} (h : s ∈ 𝓝[t] a) :
   exact nhdsWithin_le_of_mem h
 #align nhds_within_inter_of_mem nhdsWithin_inter_of_mem
 
--- porting note: new lemma
 theorem nhdsWithin_inter_of_mem' {a : α} {s t : Set α} (h : t ∈ 𝓝[s] a) : 𝓝[s ∩ t] a = 𝓝[s] a := by
   rw [inter_comm, nhdsWithin_inter_of_mem h]
+#align nhds_within_inter_of_mem' nhdsWithin_inter_of_mem'
 
 @[simp]
 theorem nhdsWithin_singleton (a : α) : 𝓝[{a}] a = pure a := by
@@ -652,6 +668,14 @@ theorem ContinuousOn.prod_map {f : α → γ} {g : β → δ} {s : Set α} {t :
   fun ⟨x, y⟩ ⟨hx, hy⟩ => ContinuousWithinAt.prod_map (hf x hx) (hg y hy)
 #align continuous_on.prod_map ContinuousOn.prod_map
 
+theorem continuous_of_cover_nhds {ι : Sort _} {f : α → β} {s : ι → Set α}
+    (hs : ∀ x : α, ∃ i, s i ∈ 𝓝 x) (hf : ∀ i, ContinuousOn f (s i)) :
+    Continuous f :=
+  continuous_iff_continuousAt.mpr fun x ↦ let ⟨i, hi⟩ := hs x; by
+    rw [ContinuousAt, ← nhdsWithin_eq_nhds.2 hi]
+    exact hf _ _ (mem_of_mem_nhds hi)
+#align continuous_of_cover_nhds continuous_of_cover_nhds
+
 theorem continuousOn_empty (f : α → β) : ContinuousOn f ∅ := fun _ => False.elim
 #align continuous_on_empty continuousOn_empty
 

Mathlib/Topology/LocallyFinite.lean

@@ -4,11 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 
 ! This file was ported from Lean 3 source module topology.locally_finite
-! leanprover-community/mathlib commit f2ce6086713c78a7f880485f7917ea547a215982
+! leanprover-community/mathlib commit 55d771df074d0dd020139ee1cd4b95521422df9f
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
-import Mathlib.Topology.Basic
+import Mathlib.Topology.ContinuousOn
 import Mathlib.Order.Filter.SmallSets
 
 /-!
@@ -77,36 +77,68 @@ theorem exists_mem_basis {ι' : Sort _} (hf : LocallyFinite f) {p : ι' → Prop
   ⟨i, hpi, hi Subset.rfl⟩
 #align locally_finite.exists_mem_basis LocallyFinite.exists_mem_basis
 
+protected theorem nhdsWithin_unionᵢ (hf : LocallyFinite f) (a : X) :
+    𝓝[⋃ i, f i] a = ⨆ i, 𝓝[f i] a := by
+  rcases hf a with ⟨U, haU, hfin⟩
+  refine le_antisymm ?_ (Monotone.le_map_supᵢ fun _ _ ↦ nhdsWithin_mono _)
+  calc
+    𝓝[⋃ i, f i] a = 𝓝[⋃ i, f i ∩ U] a := by
+      rw [← unionᵢ_inter, ← nhdsWithin_inter_of_mem' (nhdsWithin_le_nhds haU)]
+    _ = 𝓝[⋃ i ∈ {j | (f j ∩ U).Nonempty}, (f i ∩ U)] a := by
+      simp only [mem_setOf_eq, unionᵢ_nonempty_self]
+    _ = ⨆ i ∈ {j | (f j ∩ U).Nonempty}, 𝓝[f i ∩ U] a := nhdsWithin_bunionᵢ hfin _ _
+    _ ≤ ⨆ i, 𝓝[f i ∩ U] a := supᵢ₂_le_supᵢ _ _
+    _ ≤ ⨆ i, 𝓝[f i] a := supᵢ_mono fun i ↦ nhdsWithin_mono _ <| inter_subset_left _ _
+#align locally_finite.nhds_within_Union LocallyFinite.nhdsWithin_unionᵢ
+
+theorem continuousOn_unionᵢ' {g : X → Y} (hf : LocallyFinite f)
+    (hc : ∀ i x, x ∈ closure (f i) → ContinuousWithinAt g (f i) x) :
+    ContinuousOn g (⋃ i, f i) := by
+  rintro x -
+  rw [ContinuousWithinAt, hf.nhdsWithin_unionᵢ, tendsto_supᵢ]
+  intro i
+  by_cases hx : x ∈ closure (f i)
+  · exact hc i _ hx
+  · rw [mem_closure_iff_nhdsWithin_neBot, not_neBot] at hx
+    rw [hx]
+    exact tendsto_bot
+#align locally_finite.continuous_on_Union' LocallyFinite.continuousOn_unionᵢ'
+
+theorem continuousOn_unionᵢ {g : X → Y} (hf : LocallyFinite f) (h_cl : ∀ i, IsClosed (f i))
+    (h_cont : ∀ i, ContinuousOn g (f i)) : ContinuousOn g (⋃ i, f i) :=
+  hf.continuousOn_unionᵢ' fun i x hx ↦ h_cont i x <| (h_cl i).closure_subset hx
+#align locally_finite.continuous_on_Union LocallyFinite.continuousOn_unionᵢ
+
+protected theorem continuous' {g : X → Y} (hf : LocallyFinite f) (h_cov : (⋃ i, f i) = univ)
+    (hc : ∀ i x, x ∈ closure (f i) → ContinuousWithinAt g (f i) x) :
+    Continuous g :=
+  continuous_iff_continuousOn_univ.2 <| h_cov ▸ hf.continuousOn_unionᵢ' hc
+#align locally_finite.continuous' LocallyFinite.continuous'
+
+protected theorem continuous {g : X → Y} (hf : LocallyFinite f) (h_cov : (⋃ i, f i) = univ)
+    (h_cl : ∀ i, IsClosed (f i)) (h_cont : ∀ i, ContinuousOn g (f i)) :
+    Continuous g :=
+  continuous_iff_continuousOn_univ.2 <| h_cov ▸ hf.continuousOn_unionᵢ h_cl h_cont
+#align locally_finite.continuous LocallyFinite.continuous
+
 protected theorem closure (hf : LocallyFinite f) : LocallyFinite fun i => closure (f i) := by
   intro x
   rcases hf x with ⟨s, hsx, hsf⟩
   refine' ⟨interior s, interior_mem_nhds.2 hsx, hsf.subset fun i hi => _⟩
-  exact
-    (hi.mono isOpen_interior.closure_inter).of_closure.mono
-      (inter_subset_inter_right _ interior_subset)
+  exact (hi.mono isOpen_interior.closure_inter).of_closure.mono
+    (inter_subset_inter_right _ interior_subset)
 #align locally_finite.closure LocallyFinite.closure
 
+theorem closure_unionᵢ (h : LocallyFinite f) : closure (⋃ i, f i) = ⋃ i, closure (f i) := by
+  ext x
+  simp only [mem_closure_iff_nhdsWithin_neBot, h.nhdsWithin_unionᵢ, supᵢ_neBot, mem_unionᵢ]
+#align locally_finite.closure_Union LocallyFinite.closure_unionᵢ
+
 theorem isClosed_unionᵢ (hf : LocallyFinite f) (hc : ∀ i, IsClosed (f i)) :
     IsClosed (⋃ i, f i) := by
-  simp only [← isOpen_compl_iff, compl_unionᵢ, isOpen_iff_mem_nhds, mem_interᵢ]
-  intro a ha
-  replace ha : ∀ i, f iᶜ ∈ 𝓝 a := fun i => (hc i).compl_mem_nhds (ha i)
-  rcases hf a with ⟨t, h_nhds, h_fin⟩
-  have : (t ∩ ⋂ i ∈ { i | (f i ∩ t).Nonempty }, f iᶜ) ∈ 𝓝 a :=
-    inter_mem h_nhds ((binterᵢ_mem h_fin).2 fun i _ => ha i)
-  filter_upwards [this]
-  simp only [mem_inter_iff, mem_interᵢ]
-  rintro b ⟨hbt, hn⟩ i hfb
-  exact hn i ⟨b, hfb, hbt⟩ hfb
+  simp only [← closure_eq_iff_isClosed, hf.closure_unionᵢ, (hc _).closure_eq]
 #align locally_finite.is_closed_Union LocallyFinite.isClosed_unionᵢ
 
-theorem closure_unionᵢ (h : LocallyFinite f) : closure (⋃ i, f i) = ⋃ i, closure (f i) :=
-  Subset.antisymm
-    (closure_minimal (unionᵢ_mono fun _ => subset_closure) <|
-      h.closure.isClosed_unionᵢ fun _ => isClosed_closure)
-    (unionᵢ_subset fun _ => closure_mono <| subset_unionᵢ _ _)
-#align locally_finite.closure_Union LocallyFinite.closure_unionᵢ
-
 /-- If `f : β → set α` is a locally finite family of closed sets, then for any `x : α`, the
 intersection of the complements to `f i`, `x ∉ f i`, is a neighbourhood of `x`. -/
 theorem interᵢ_compl_mem_nhds (hf : LocallyFinite f) (hc : ∀ i, IsClosed (f i)) (x : X) :

Mathlib/Topology/SubsetProperties.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Mario Carneiro, Yury Kudryashov
 
 ! This file was ported from Lean 3 source module topology.subset_properties
-! leanprover-community/mathlib commit 59694bd07f0a39c5beccba34bd9f413a160782bf
+! leanprover-community/mathlib commit 55d771df074d0dd020139ee1cd4b95521422df9f
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -14,6 +14,7 @@ import Mathlib.Data.Finset.Order
 import Mathlib.Data.Set.Accumulate
 import Mathlib.Data.Set.BoolIndicator
 import Mathlib.Topology.Bornology.Basic
+import Mathlib.Topology.LocallyFinite
 import Mathlib.Order.Minimal
 
 /-!