feat(topology/*): add lemmas about 𝓝[⋃ i, s i] a (#18321)

* Add `theorem nhds_within_eq_nhds`, `nhds_within_bUnion`, `nhds_within_sUnion`, `nhds_within_Union`, `nhds_within_inter_of_mem'`.

* Add `locally_finite.nhds_within_Union`, use it to golf `locally_finite.is_closed_Union` and `locally_finite.closure_Union`.

* Reformulate `continuous_subtype_nhds_cover` in terms of `continuous_on`, rename to `continuous_of_cover_nhds`.

* Reformulate `continuous_subtype_is_closed_cover` in terms of `continuous_on`, several versions are named `locally_finite.continuous_on_Union`, `locally_finite.continuous`, and primed versions of these lemmas.

* Reorder imports.



Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

src/data/analysis/topology.lean

@@ -5,6 +5,7 @@ Authors: Mario Carneiro
 -/
 import data.analysis.filter
 import topology.bases
+import topology.locally_finite
 
 /-!
 # Computational realization of topological spaces (experimental)

src/topology/constructions.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Mario Carneiro, Patrick Massot
 -/
 import topology.maps
-import topology.locally_finite
 import order.filter.pi
 
 /-!
@@ -866,43 +865,6 @@ lemma tendsto_subtype_rng {β : Type*} {p : α → Prop} {b : filter β} {f : β
   ∀{a:subtype p}, tendsto f b (𝓝 a) ↔ tendsto (λx, (f x : α)) b (𝓝 (a : α))
 | ⟨a, ha⟩ := by rw [nhds_subtype_eq_comap, tendsto_comap_iff, subtype.coe_mk]
 
-lemma continuous_subtype_nhds_cover {ι : Sort*} {f : α → β} {c : ι → α → Prop}
-  (c_cover : ∀x:α, ∃i, {x | c i x} ∈ 𝓝 x)
-  (f_cont  : ∀i, continuous (λ(x : subtype (c i)), f x)) :
-  continuous f :=
-continuous_iff_continuous_at.mpr $ assume x,
-  let ⟨i, (c_sets : {x | c i x} ∈ 𝓝 x)⟩ := c_cover x in
-  let x' : subtype (c i) := ⟨x, mem_of_mem_nhds c_sets⟩ in
-  calc map f (𝓝 x) = map f (map coe (𝓝 x')) :
-      congr_arg (map f) (map_nhds_subtype_coe_eq _ $ c_sets).symm
-    ... = map (λx:subtype (c i), f x) (𝓝 x') : rfl
-    ... ≤ 𝓝 (f x) : continuous_iff_continuous_at.mp (f_cont i) x'
-
-lemma continuous_subtype_is_closed_cover {ι : Sort*} {f : α → β} (c : ι → α → Prop)
-  (h_lf : locally_finite (λi, {x | c i x}))
-  (h_is_closed : ∀i, is_closed {x | c i x})
-  (h_cover : ∀x, ∃i, c i x)
-  (f_cont  : ∀i, continuous (λ(x : subtype (c i)), f x)) :
-  continuous f :=
-continuous_iff_is_closed.mpr $
-  assume s hs,
-  have ∀i, is_closed ((coe : {x | c i x} → α) '' (f ∘ coe ⁻¹' s)),
-    from assume i,
-    (closed_embedding_subtype_coe (h_is_closed _)).is_closed_map _ (hs.preimage (f_cont i)),
-  have is_closed (⋃i, (coe : {x | c i x} → α) '' (f ∘ coe ⁻¹' s)),
-    from locally_finite.is_closed_Union
-      (h_lf.subset $ assume i x ⟨⟨x', hx'⟩, _, heq⟩, heq ▸ hx')
-      this,
-  have f ⁻¹' s = (⋃i, (coe : {x | c i x} → α) '' (f ∘ coe ⁻¹' s)),
-  begin
-    apply set.ext,
-    have : ∀ (x : α), f x ∈ s ↔ ∃ (i : ι), c i x ∧ f x ∈ s :=
-      λ x, ⟨λ hx, let ⟨i, hi⟩ := h_cover x in ⟨i, hi, hx⟩,
-            λ ⟨i, hi, hx⟩, hx⟩,
-    simpa [and.comm, @and.left_comm (c _ _), ← exists_and_distrib_right],
-  end,
-  by rwa [this]
-
 lemma closure_subtype {x : {a // p a}} {s : set {a // p a}}:
   x ∈ closure s ↔ (x : α) ∈ closure ((coe : _ → α) '' s) :=
 closure_induced

src/topology/continuous_function/basic.lean

@@ -258,11 +258,9 @@ begin
     rw set.mem_Union,
     obtain ⟨i, hi⟩ := hS x,
     exact ⟨i, mem_of_mem_nhds hi⟩ },
-  refine ⟨set.lift_cover S (λ i, φ i) hφ H, continuous_subtype_nhds_cover hS _⟩,
-  intros i,
-  convert (φ i).continuous,
-  ext x,
-  exact set.lift_cover_coe x,
+  refine ⟨set.lift_cover S (λ i, φ i) hφ H, continuous_of_cover_nhds hS $ λ i, _⟩,
+  rw [continuous_on_iff_continuous_restrict],
+  simpa only [set.restrict, set.lift_cover_coe] using (φ i).continuous
 end
 
 variables {S φ hφ hS}

src/topology/continuous_on.lean

@@ -215,9 +215,12 @@ theorem nhds_within_eq_nhds_within {a : α} {s t u : set α}
   𝓝[t] a = 𝓝[u] a :=
 by rw [nhds_within_restrict t h₀ h₁, nhds_within_restrict u h₀ h₁, h₂]
 
+@[simp] theorem nhds_within_eq_nhds {a : α} {s : set α} : 𝓝[s] a = 𝓝 a ↔ s ∈ 𝓝 a :=
+by rw [nhds_within, inf_eq_left, le_principal_iff]
+
 theorem is_open.nhds_within_eq {a : α} {s : set α} (h : is_open s) (ha : a ∈ s) :
   𝓝[s] a = 𝓝 a :=
-inf_eq_left.2 $ le_principal_iff.2 $ is_open.mem_nhds h ha
+nhds_within_eq_nhds.2 $ is_open.mem_nhds h ha
 
 lemma preimage_nhds_within_coinduced {π : α → β} {s : set β} {t : set α} {a : α}
   (h : a ∈ t) (ht : is_open t)
@@ -232,6 +235,18 @@ theorem nhds_within_union (a : α) (s t : set α) :
   𝓝[s ∪ t] a = 𝓝[s] a ⊔ 𝓝[t] a :=
 by { delta nhds_within, rw [←inf_sup_left, sup_principal] }
 
+theorem nhds_within_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) $ λ t T _ _ hT,
+  by simp only [hT, nhds_within_union, supr_insert, bUnion_insert]
+
+theorem nhds_within_sUnion {S : set (set α)} (hS : S.finite) (a : α) :
+  𝓝[⋃₀ S] a = ⨆ s ∈ S, 𝓝[s] a :=
+by rw [sUnion_eq_bUnion, nhds_within_bUnion hS]
+
+theorem nhds_within_Union {ι} [finite ι] (s : ι → set α) (a : α) : 𝓝[⋃ i, s i] a = ⨆ i, 𝓝[s i] a :=
+by rw [← sUnion_range, nhds_within_sUnion (finite_range s), supr_range]
+
 theorem nhds_within_inter (a : α) (s t : set α) :
   𝓝[s ∩ t] a = 𝓝[s] a ⊓ 𝓝[t] a :=
 by { delta nhds_within, rw [inf_left_comm, inf_assoc, inf_principal, ←inf_assoc, inf_idem] }
@@ -244,6 +259,10 @@ theorem nhds_within_inter_of_mem {a : α} {s t : set α} (h : s ∈ 𝓝[t] a) :
   𝓝[s ∩ t] a = 𝓝[t] a :=
 by { rw [nhds_within_inter, inf_eq_right], exact nhds_within_le_of_mem h }
 
+theorem nhds_within_inter_of_mem' {a : α} {s t : set α} (h : s ∈ 𝓝[t] a) :
+  𝓝[t ∩ s] a = 𝓝[t] a :=
+by rw [inter_comm, nhds_within_inter_of_mem h]
+
 @[simp] theorem nhds_within_singleton (a : α) : 𝓝[{a}] a = pure a :=
 by rw [nhds_within, principal_singleton, inf_eq_right.2 (pure_le_nhds a)]
 
@@ -599,6 +618,12 @@ lemma continuous_on.prod_map {f : α → γ} {g : β → δ} {s : set α} {t : s
   continuous_on (prod.map f g) (s ×ˢ t) :=
 λ ⟨x, y⟩ ⟨hx, hy⟩, continuous_within_at.prod_map (hf x hx) (hg y hy)
 
+lemma continuous_of_cover_nhds {ι : Sort*} {f : α → β} {s : ι → set α}
+  (hs : ∀ x : α, ∃ i, s i ∈ 𝓝 x) (hf : ∀ i, continuous_on f (s i)) :
+  continuous f :=
+continuous_iff_continuous_at.mpr $ λ x, let ⟨i, hi⟩ := hs x in
+  by { rw [continuous_at, ← nhds_within_eq_nhds.2 hi], exact hf _ _ (mem_of_mem_nhds hi) }
+
 lemma continuous_on_empty (f : α → β) : continuous_on f ∅ :=
 λ x, false.elim
 

src/topology/locally_finite.lean

@@ -3,7 +3,7 @@ Copyright (c) 2022 Yury Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
-import topology.basic
+import topology.continuous_on
 import order.filter.small_sets
 
 /-!
@@ -69,6 +69,50 @@ lemma exists_mem_basis {ι' : Sort*} (hf : locally_finite f) {p : ι' → Prop}
 let ⟨i, hpi, hi⟩ := hb.small_sets.eventually_iff.mp (hf.eventually_small_sets x)
 in ⟨i, hpi, hi subset.rfl⟩
 
+protected theorem nhds_within_Union (hf : locally_finite f) (a : X) :
+  𝓝[⋃ i, f i] a = ⨆ i, 𝓝[f i] a :=
+begin
+  rcases hf a with ⟨U, haU, hfin⟩,
+  refine le_antisymm _ (supr_le $ λ i, nhds_within_mono _ (subset_Union _ _)),
+  calc 𝓝[⋃ i, f i] a = 𝓝[⋃ i, f i ∩ U] a :
+    by rw [← Union_inter, ← nhds_within_inter_of_mem' (nhds_within_le_nhds haU)]
+  ... = 𝓝[⋃ i ∈ {j | (f j ∩ U).nonempty}, (f i ∩ U)] a :
+    by simp only [mem_set_of_eq, Union_nonempty_self]
+  ... = ⨆ i ∈ {j | (f j ∩ U).nonempty}, 𝓝[f i ∩ U] a :
+    nhds_within_bUnion hfin _ _
+  ... ≤ ⨆ i, 𝓝[f i ∩ U] a : supr₂_le_supr _ _
+  ... ≤ ⨆ i, 𝓝[f i] a : supr_mono (λ i, nhds_within_mono _ $ inter_subset_left _ _)
+end
+
+lemma continuous_on_Union' {g : X → Y} (hf : locally_finite f)
+  (hc : ∀ i x, x ∈ closure (f i) → continuous_within_at g (f i) x) :
+  continuous_on g (⋃ i, f i) :=
+begin
+  rintro x -,
+  rw [continuous_within_at, hf.nhds_within_Union, tendsto_supr],
+  intro i,
+  by_cases hx : x ∈ closure (f i),
+  { exact hc i _ hx },
+  { rw [mem_closure_iff_nhds_within_ne_bot, not_ne_bot] at hx,
+    rw [hx],
+    exact tendsto_bot }
+end
+
+lemma continuous_on_Union {g : X → Y} (hf : locally_finite f) (h_cl : ∀ i, is_closed (f i))
+  (h_cont : ∀ i, continuous_on g (f i)) :
+  continuous_on g (⋃ i, f i) :=
+hf.continuous_on_Union' $ λ i x hx, h_cont i x $ (h_cl i).closure_subset hx
+
+protected lemma continuous' {g : X → Y} (hf : locally_finite f) (h_cov : (⋃ i, f i) = univ)
+  (hc : ∀ i x, x ∈ closure (f i) → continuous_within_at g (f i) x) :
+  continuous g :=
+continuous_iff_continuous_on_univ.2 $ h_cov ▸ hf.continuous_on_Union' hc
+
+protected lemma continuous {g : X → Y} (hf : locally_finite f) (h_cov : (⋃ i, f i) = univ)
+  (h_cl : ∀ i, is_closed (f i)) (h_cont : ∀ i, continuous_on g (f i)) :
+  continuous g :=
+continuous_iff_continuous_on_univ.2 $ h_cov ▸ hf.continuous_on_Union h_cl h_cont
+
 protected lemma closure (hf : locally_finite f) : locally_finite (λ i, closure (f i)) :=
 begin
   intro x,
@@ -78,26 +122,15 @@ begin
     (inter_subset_inter_right _ interior_subset)
 end
 
-lemma is_closed_Union (hf : locally_finite f) (hc : ∀i, is_closed (f i)) :
-  is_closed (⋃i, f i) :=
+lemma closure_Union (h : locally_finite f) : closure (⋃ i, f i) = ⋃ i, closure (f i) :=
 begin
-  simp only [← is_open_compl_iff, compl_Union, is_open_iff_mem_nhds, mem_Inter],
-  intros a ha,
-  replace ha : ∀ i, (f i)ᶜ ∈ 𝓝 a := λ i, (hc i).is_open_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,
-    from inter_mem h_nhds ((bInter_mem h_fin).2 (λ i _, ha i)),
-  filter_upwards [this],
-  simp only [mem_inter_iff, mem_Inter],
-  rintros b ⟨hbt, hn⟩ i hfb,
-  exact hn i ⟨b, hfb, hbt⟩ hfb,
+  ext x,
+  simp only [mem_closure_iff_nhds_within_ne_bot, h.nhds_within_Union, supr_ne_bot, mem_Union]
 end
 
-lemma closure_Union (h : locally_finite f) : closure (⋃ i, f i) = ⋃ i, closure (f i) :=
-subset.antisymm
-  (closure_minimal (Union_mono $ λ _, subset_closure) $
-    h.closure.is_closed_Union $ λ _, is_closed_closure)
-  (Union_subset $ λ i, closure_mono $ subset_Union _ _)
+lemma is_closed_Union (hf : locally_finite f) (hc : ∀ i, is_closed (f i)) :
+  is_closed (⋃ i, f i) :=
+by simp only [← closure_eq_iff_is_closed, hf.closure_Union, (hc _).closure_eq]
 
 /-- 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`. -/

src/topology/subset_properties.lean

@@ -9,6 +9,7 @@ import data.finset.order
 import data.set.accumulate
 import data.set.bool_indicator
 import topology.bornology.basic
+import topology.locally_finite
 import order.minimal
 
 /-!