chore(topology/locally_finite): move from topology.basic (#15640)

Create a new file about `locally_finite`, move the definition and some lemmas from `topology.basic`.

Author: urkud

src/topology/basic.lean

@@ -1175,151 +1175,6 @@ le_nhds_Lim h
 
 end lim
 
-/-!
-### Locally finite families
--/
-
-/- locally finite family [General Topology (Bourbaki, 1995)] -/
-section locally_finite
-
-/-- A family of sets in `set α` is locally finite if at every point `x:α`,
-  there is a neighborhood of `x` which meets only finitely many sets in the family -/
-def locally_finite (f : β → set α) :=
-∀x:α, ∃t ∈ 𝓝 x, {i | (f i ∩ t).nonempty}.finite
-
-lemma locally_finite.point_finite {f : β → set α} (hf : locally_finite f) (x : α) :
-  {b | x ∈ f b}.finite :=
-let ⟨t, hxt, ht⟩ := hf x in ht.subset $ λ b hb, ⟨x, hb, mem_of_mem_nhds hxt⟩
-
-lemma locally_finite_of_finite [finite β] (f : β → set α) : locally_finite f :=
-assume x, ⟨univ, univ_mem, to_finite _⟩
-
-lemma locally_finite.subset
-  {f₁ f₂ : β → set α} (hf₂ : locally_finite f₂) (hf : ∀b, f₁ b ⊆ f₂ b) : locally_finite f₁ :=
-assume a,
-let ⟨t, ht₁, ht₂⟩ := hf₂ a in
-⟨t, ht₁, ht₂.subset $ assume i hi, hi.mono $ inter_subset_inter (hf i) $ subset.refl _⟩
-
-lemma locally_finite.comp_inj_on {ι} {f : β → set α} {g : ι → β} (hf : locally_finite f)
-  (hg : inj_on g {i | (f (g i)).nonempty}) : locally_finite (f ∘ g) :=
-λ x, let ⟨t, htx, htf⟩ := hf x in ⟨t, htx, htf.preimage $ hg.mono $ λ i hi,
-  hi.out.mono $ inter_subset_left _ _⟩
-
-lemma locally_finite.comp_injective {ι} {f : β → set α} {g : ι → β} (hf : locally_finite f)
-  (hg : function.injective g) : locally_finite (f ∘ g) :=
-hf.comp_inj_on (hg.inj_on _)
-
-lemma locally_finite.eventually_finite {f : β → set α} (hf : locally_finite f) (x : α) :
-  ∀ᶠ s in (𝓝 x).small_sets, {i | (f i ∩ s).nonempty}.finite :=
-eventually_small_sets.2 $ let ⟨s, hsx, hs⟩ := hf x in
-  ⟨s, hsx, λ t hts, hs.subset $ λ i hi, hi.out.mono $ inter_subset_inter_right _ hts⟩
-
-lemma locally_finite.exists_mem_basis {f : β → set α} (hf : locally_finite f) {p : ι → Prop}
-  {s : ι → set α} {x : α} (hb : (𝓝 x).has_basis p s) :
-  ∃ i (hi : p i), {j | (f j ∩ s i).nonempty}.finite :=
-let ⟨i, hpi, hi⟩ := hb.small_sets.eventually_iff.mp (hf.eventually_finite x)
-in ⟨i, hpi, hi subset.rfl⟩
-
-lemma locally_finite.sum_elim {γ} {f : β → set α} {g : γ → set α} (hf : locally_finite f)
-  (hg : locally_finite g) : locally_finite (sum.elim f g) :=
-begin
-  intro x,
-  obtain ⟨s, hsx, hsf, hsg⟩ :
-    ∃ s, s ∈ 𝓝 x ∧ {i | (f i ∩ s).nonempty}.finite ∧ {j | (g j ∩ s).nonempty}.finite,
-    from ((𝓝 x).frequently_small_sets_mem.and_eventually
-      ((hf.eventually_finite x).and (hg.eventually_finite x))).exists,
-  refine ⟨s, hsx, _⟩,
-  convert (hsf.image sum.inl).union (hsg.image sum.inr) using 1,
-  ext (i|j); simp
-end
-
-lemma locally_finite.closure {f : β → set α} (hf : locally_finite f) :
-  locally_finite (λ i, closure (f i)) :=
-begin
-  intro x,
-  rcases hf x with ⟨s, hsx, hsf⟩,
-  refine ⟨interior s, interior_mem_nhds.2 hsx, hsf.subset $ λ i hi, _⟩,
-  exact (hi.mono (closure_inter_open' is_open_interior)).of_closure.mono
-    (inter_subset_inter_right _ interior_subset)
-end
-
-lemma locally_finite.is_closed_Union {f : β → set α}
-  (h₁ : locally_finite f) (h₂ : ∀i, is_closed (f i)) : is_closed (⋃i, 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, (h₂ i).is_open_compl.mem_nhds (ha i),
-  rcases h₁ 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_eq, mem_Inter],
-  rintros b ⟨hbt, hn⟩ i hfb,
-  exact hn i ⟨b, hfb, hbt⟩ hfb,
-end
-
-lemma locally_finite.closure_Union {f : β → set α} (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 _ _)
-
-/-- 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`. -/
-lemma locally_finite.Inter_compl_mem_nhds {f : β → set α} (hf : locally_finite f)
-  (hc : ∀ i, is_closed (f i)) (x : α) : (⋂ i (hi : x ∉ f i), (f i)ᶜ) ∈ 𝓝 x :=
-begin
-  refine is_open.mem_nhds _ (mem_Inter₂.2 $ λ i, id),
-  suffices : is_closed (⋃ i : {i // x ∉ f i}, f i),
-    by rwa [← is_open_compl_iff, compl_Union, Inter_subtype] at this,
-  exact (hf.comp_injective subtype.coe_injective).is_closed_Union (λ i, hc _)
-end
-
-/-- Let `f : ℕ → Π a, β a` be a sequence of (dependent) functions on a topological space. Suppose
-that the family of sets `s n = {x | f (n + 1) x ≠ f n x}` is locally finite. Then there exists a
-function `F : Π a, β a` such that for any `x`, we have `f n x = F x` on the product of an infinite
-interval `[N, +∞)` and a neighbourhood of `x`.
-
-We formulate the conclusion in terms of the product of filter `filter.at_top` and `𝓝 x`. -/
-lemma locally_finite.exists_forall_eventually_eq_prod {β : α → Sort*} {f : ℕ → Π a : α, β a}
-  (hf : locally_finite (λ n, {x | f (n + 1) x ≠ f n x})) :
-  ∃ F : Π a : α, β a, ∀ x, ∀ᶠ p : ℕ × α in at_top ×ᶠ 𝓝 x, f p.1 p.2 = F p.2 :=
-begin
-  choose U hUx hU using hf,
-  choose N hN using λ x, (hU x).bdd_above,
-  replace hN : ∀ x (n > N x) (y ∈ U x), f (n + 1) y = f n y,
-    from λ x n hn y hy, by_contra (λ hne, hn.lt.not_le $ hN x ⟨y, hne, hy⟩),
-  replace hN : ∀ x (n ≥ N x + 1) (y ∈ U x), f n y = f (N x + 1) y,
-    from λ x n hn y hy, nat.le_induction rfl (λ k hle, (hN x _ hle _ hy).trans) n hn, 
-  refine ⟨λ x, f (N x + 1) x, λ x, _⟩,
-  filter_upwards [filter.prod_mem_prod (eventually_gt_at_top (N x)) (hUx x)],
-  rintro ⟨n, y⟩ ⟨hn : N x < n, hy : y ∈ U x⟩,
-  calc f n y = f (N x + 1) y : hN _ _ hn _ hy
-  ... = f (max (N x + 1) (N y + 1)) y : (hN _ _ (le_max_left _ _) _ hy).symm
-  ... = f (N y + 1) y : hN _ _ (le_max_right _ _) _ (mem_of_mem_nhds $ hUx y)
-end
-
-/-- Let `f : ℕ → Π a, β a` be a sequence of (dependent) functions on a topological space. Suppose
-that the family of sets `s n = {x | f (n + 1) x ≠ f n x}` is locally finite. Then there exists a
-function `F : Π a, β a` such that for any `x`, for sufficiently large values of `n`, we have
-`f n y = F y` in a neighbourhood of `x`. -/
-lemma locally_finite.exists_forall_eventually_at_top_eventually_eq' {β : α → Sort*}
-  {f : ℕ → Π a : α, β a} (hf : locally_finite (λ n, {x | f (n + 1) x ≠ f n x})) :
-  ∃ F : Π a : α, β a, ∀ x, ∀ᶠ n : ℕ in at_top, ∀ᶠ y : α in 𝓝 x, f n y = F y :=
-hf.exists_forall_eventually_eq_prod.imp $ λ F hF x, (hF x).curry
-
-/-- Let `f : ℕ → α → β` be a sequence of functions on a topological space. Suppose
-that the family of sets `s n = {x | f (n + 1) x ≠ f n x}` is locally finite. Then there exists a
-function `F :  α → β` such that for any `x`, for sufficiently large values of `n`, we have
-`f n =ᶠ[𝓝 x] F`. -/
-lemma locally_finite.exists_forall_eventually_at_top_eventually_eq
-  {f : ℕ → α → β} (hf : locally_finite (λ n, {x | f (n + 1) x ≠ f n x})) :
-  ∃ F : α → β, ∀ x, ∀ᶠ n : ℕ in at_top, f n =ᶠ[𝓝 x] F :=
-hf.exists_forall_eventually_at_top_eventually_eq'
-
-end locally_finite
-
 end topological_space
 
 /-!
@@ -1446,11 +1301,6 @@ nat.rec_on n continuous_at_id $ λ n ihn,
 show continuous_at (f^[n] ∘ f) x,
 from continuous_at.comp (hx.symm ▸ ihn) hf
 
-lemma locally_finite.preimage_continuous {ι} {f : ι → set α} {g : β → α} (hf : locally_finite f)
-  (hg : continuous g) : locally_finite (λ i, g ⁻¹' (f i)) :=
-λ x, let ⟨s, hsx, hs⟩ := hf (g x)
-  in ⟨g ⁻¹' s, hg.continuous_at hsx, hs.subset $ λ i ⟨y, hy⟩, ⟨g y, hy⟩⟩
-
 lemma continuous_iff_is_closed {f : α → β} :
   continuous f ↔ (∀s, is_closed s → is_closed (f ⁻¹' s)) :=
 ⟨assume hf s hs, by simpa using (continuous_def.1 hf sᶜ hs.is_open_compl).is_closed_compl,

src/topology/constructions.lean

@@ -4,6 +4,7 @@ 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
 import data.fin.tuple
 

src/topology/locally_finite.lean

@@ -0,0 +1,164 @@
+/-
+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
+
+/-!
+### Locally finite families of sets
+
+We say that a family of sets in a topological space is *locally finite* if at every point `x : X`,
+there is a neighborhood of `x` which meets only finitely many sets in the family.
+
+In this file we give the definition and prove basic properties of locally finite families of sets.
+-/
+
+/- locally finite family [General Topology (Bourbaki, 1995)] -/
+
+open set function filter
+open_locale topological_space filter
+
+variables {ι ι' α X Y : Type*} [topological_space X] [topological_space Y]
+  {f g : ι → set X}
+
+/-- A family of sets in `set X` is locally finite if at every point `x : X`,
+there is a neighborhood of `x` which meets only finitely many sets in the family. -/
+def locally_finite (f : ι → set X) :=
+∀ x : X, ∃t ∈ 𝓝 x, {i | (f i ∩ t).nonempty}.finite
+
+lemma locally_finite_of_finite [finite ι] (f : ι → set X) : locally_finite f :=
+assume x, ⟨univ, univ_mem, to_finite _⟩
+
+namespace locally_finite
+
+lemma point_finite (hf : locally_finite f) (x : X) : {b | x ∈ f b}.finite :=
+let ⟨t, hxt, ht⟩ := hf x in ht.subset $ λ b hb, ⟨x, hb, mem_of_mem_nhds hxt⟩
+
+protected lemma subset (hf : locally_finite f) (hg : ∀ i, g i ⊆ f i) : locally_finite g :=
+assume a,
+let ⟨t, ht₁, ht₂⟩ := hf a in
+⟨t, ht₁, ht₂.subset $ assume i hi, hi.mono $ inter_subset_inter (hg i) subset.rfl⟩
+
+lemma comp_inj_on {g : ι' → ι} (hf : locally_finite f)
+  (hg : inj_on g {i | (f (g i)).nonempty}) : locally_finite (f ∘ g) :=
+λ x, let ⟨t, htx, htf⟩ := hf x in ⟨t, htx, htf.preimage $ hg.mono $ λ i hi,
+  hi.out.mono $ inter_subset_left _ _⟩
+
+lemma comp_injective {g : ι' → ι} (hf : locally_finite f)
+  (hg : function.injective g) : locally_finite (f ∘ g) :=
+hf.comp_inj_on (hg.inj_on _)
+
+lemma eventually_finite (hf : locally_finite f) (x : X) :
+  ∀ᶠ s in (𝓝 x).small_sets, {i | (f i ∩ s).nonempty}.finite :=
+eventually_small_sets.2 $ let ⟨s, hsx, hs⟩ := hf x in
+  ⟨s, hsx, λ t hts, hs.subset $ λ i hi, hi.out.mono $ inter_subset_inter_right _ hts⟩
+
+lemma exists_mem_basis {ι' : Sort*} (hf : locally_finite f) {p : ι' → Prop}
+  {s : ι' → set X} {x : X} (hb : (𝓝 x).has_basis p s) :
+  ∃ i (hi : p i), {j | (f j ∩ s i).nonempty}.finite :=
+let ⟨i, hpi, hi⟩ := hb.small_sets.eventually_iff.mp (hf.eventually_finite x)
+in ⟨i, hpi, hi subset.rfl⟩
+
+lemma sum_elim {g : ι' → set X} (hf : locally_finite f) (hg : locally_finite g) :
+  locally_finite (sum.elim f g) :=
+begin
+  intro x,
+  obtain ⟨s, hsx, hsf, hsg⟩ :
+    ∃ s, s ∈ 𝓝 x ∧ {i | (f i ∩ s).nonempty}.finite ∧ {j | (g j ∩ s).nonempty}.finite,
+    from ((𝓝 x).frequently_small_sets_mem.and_eventually
+      ((hf.eventually_finite x).and (hg.eventually_finite x))).exists,
+  refine ⟨s, hsx, _⟩,
+  convert (hsf.image sum.inl).union (hsg.image sum.inr) using 1,
+  ext (i|j); simp
+end
+
+protected lemma closure (hf : locally_finite f) : locally_finite (λ i, closure (f i)) :=
+begin
+  intro x,
+  rcases hf x with ⟨s, hsx, hsf⟩,
+  refine ⟨interior s, interior_mem_nhds.2 hsx, hsf.subset $ λ i hi, _⟩,
+  exact (hi.mono (closure_inter_open' is_open_interior)).of_closure.mono
+    (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) :=
+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_eq, mem_Inter],
+  rintros b ⟨hbt, hn⟩ i hfb,
+  exact hn i ⟨b, hfb, hbt⟩ hfb,
+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 _ _)
+
+/-- 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`. -/
+lemma Inter_compl_mem_nhds (hf : locally_finite f) (hc : ∀ i, is_closed (f i)) (x : X) :
+  (⋂ i (hi : x ∉ f i), (f i)ᶜ) ∈ 𝓝 x :=
+begin
+  refine is_open.mem_nhds _ (mem_Inter₂.2 $ λ i, id),
+  suffices : is_closed (⋃ i : {i // x ∉ f i}, f i),
+    by rwa [← is_open_compl_iff, compl_Union, Inter_subtype] at this,
+  exact (hf.comp_injective subtype.coe_injective).is_closed_Union (λ i, hc _)
+end
+
+/-- Let `f : ℕ → Π a, β a` be a sequence of (dependent) functions on a topological space. Suppose
+that the family of sets `s n = {x | f (n + 1) x ≠ f n x}` is locally finite. Then there exists a
+function `F : Π a, β a` such that for any `x`, we have `f n x = F x` on the product of an infinite
+interval `[N, +∞)` and a neighbourhood of `x`.
+
+We formulate the conclusion in terms of the product of filter `filter.at_top` and `𝓝 x`. -/
+lemma exists_forall_eventually_eq_prod {π : X → Sort*} {f : ℕ → Π x : X, π x}
+  (hf : locally_finite (λ n, {x | f (n + 1) x ≠ f n x})) :
+  ∃ F : Π x : X, π x, ∀ x, ∀ᶠ p : ℕ × X in at_top ×ᶠ 𝓝 x, f p.1 p.2 = F p.2 :=
+begin
+  choose U hUx hU using hf,
+  choose N hN using λ x, (hU x).bdd_above,
+  replace hN : ∀ x (n > N x) (y ∈ U x), f (n + 1) y = f n y,
+    from λ x n hn y hy, by_contra (λ hne, hn.lt.not_le $ hN x ⟨y, hne, hy⟩),
+  replace hN : ∀ x (n ≥ N x + 1) (y ∈ U x), f n y = f (N x + 1) y,
+    from λ x n hn y hy, nat.le_induction rfl (λ k hle, (hN x _ hle _ hy).trans) n hn, 
+  refine ⟨λ x, f (N x + 1) x, λ x, _⟩,
+  filter_upwards [filter.prod_mem_prod (eventually_gt_at_top (N x)) (hUx x)],
+  rintro ⟨n, y⟩ ⟨hn : N x < n, hy : y ∈ U x⟩,
+  calc f n y = f (N x + 1) y : hN _ _ hn _ hy
+  ... = f (max (N x + 1) (N y + 1)) y : (hN _ _ (le_max_left _ _) _ hy).symm
+  ... = f (N y + 1) y : hN _ _ (le_max_right _ _) _ (mem_of_mem_nhds $ hUx y)
+end
+
+/-- Let `f : ℕ → Π a, β a` be a sequence of (dependent) functions on a topological space. Suppose
+that the family of sets `s n = {x | f (n + 1) x ≠ f n x}` is locally finite. Then there exists a
+function `F : Π a, β a` such that for any `x`, for sufficiently large values of `n`, we have
+`f n y = F y` in a neighbourhood of `x`. -/
+lemma exists_forall_eventually_at_top_eventually_eq' {π : X → Sort*}
+  {f : ℕ → Π x : X, π x} (hf : locally_finite (λ n, {x | f (n + 1) x ≠ f n x})) :
+  ∃ F : Π x : X, π x, ∀ x, ∀ᶠ n : ℕ in at_top, ∀ᶠ y : X in 𝓝 x, f n y = F y :=
+hf.exists_forall_eventually_eq_prod.imp $ λ F hF x, (hF x).curry
+
+/-- Let `f : ℕ → α → β` be a sequence of functions on a topological space. Suppose
+that the family of sets `s n = {x | f (n + 1) x ≠ f n x}` is locally finite. Then there exists a
+function `F :  α → β` such that for any `x`, for sufficiently large values of `n`, we have
+`f n =ᶠ[𝓝 x] F`. -/
+lemma exists_forall_eventually_at_top_eventually_eq {f : ℕ → X → α}
+  (hf : locally_finite (λ n, {x | f (n + 1) x ≠ f n x})) :
+  ∃ F : X → α, ∀ x, ∀ᶠ n : ℕ in at_top, f n =ᶠ[𝓝 x] F :=
+hf.exists_forall_eventually_at_top_eventually_eq'
+
+lemma preimage_continuous {g : Y → X} (hf : locally_finite f) (hg : continuous g) :
+  locally_finite (λ i, g ⁻¹' (f i)) :=
+λ x, let ⟨s, hsx, hs⟩ := hf (g x)
+  in ⟨g ⁻¹' s, hg.continuous_at hsx, hs.subset $ λ i ⟨y, hy⟩, ⟨g y, hy⟩⟩
+
+end locally_finite