feat(topology/locally_finite): add lemmas about option _ and sum _ _ (#15923)

Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>

Author: urkud

src/data/set/basic.lean

@@ -2158,6 +2158,11 @@ is_compl.compl_eq is_compl_range_inl_range_inr
 @[simp] lemma compl_range_inr : (range (sum.inr : β → α ⊕ β))ᶜ = range (sum.inl : α → α ⊕ β) :=
 is_compl.compl_eq is_compl_range_inl_range_inr.symm
 
+theorem image_preimage_inl_union_image_preimage_inr (s : set (α ⊕ β)) :
+  sum.inl '' (sum.inl ⁻¹' s) ∪ sum.inr '' (sum.inr ⁻¹' s) = s :=
+by rw [image_preimage_eq_inter_range, image_preimage_eq_inter_range, ← inter_distrib_left,
+  range_inl_union_range_inr, inter_univ]
+
 @[simp] theorem range_quot_mk (r : α → α → Prop) : range (quot.mk r) = univ :=
 (surjective_quot_mk r).range_eq
 

src/data/set/finite.lean

@@ -597,6 +597,11 @@ theorem finite_mem_finset (s : finset α) : {a | a ∈ s}.finite := to_finite _
 lemma subsingleton.finite {s : set α} (h : s.subsingleton) : s.finite :=
 h.induction_on finite_empty finite_singleton
 
+lemma finite_preimage_inl_and_inr {s : set (α ⊕ β)} :
+  (sum.inl ⁻¹' s).finite ∧ (sum.inr ⁻¹' s).finite ↔ s.finite :=
+⟨λ h, image_preimage_inl_union_image_preimage_inr s ▸ (h.1.image _).union (h.2.image _),
+  λ h, ⟨h.preimage (sum.inl_injective.inj_on _), h.preimage (sum.inr_injective.inj_on _)⟩⟩
+
 theorem exists_finite_iff_finset {p : set α → Prop} :
   (∃ s : set α, s.finite ∧ p s) ↔ ∃ s : finset α, p ↑s :=
 ⟨λ ⟨s, hs, hps⟩, ⟨hs.to_finset, hs.coe_to_finset.symm ▸ hps⟩,

src/topology/locally_finite.lean

@@ -19,7 +19,8 @@ In this file we give the definition and prove basic properties of locally finite
 open set function filter
 open_locale topological_space filter
 
-variables {ι ι' α X Y : Type*} [topological_space X] [topological_space Y]
+universe u
+variables {ι : Type u} {ι' α 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`,
@@ -45,34 +46,25 @@ lemma comp_inj_on {g : ι' → ι} (hf : locally_finite f)
 λ 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) :=
+lemma comp_injective {g : ι' → ι} (hf : locally_finite f) (hg : injective g) :
+  locally_finite (f ∘ g) :=
 hf.comp_inj_on (hg.inj_on _)
 
-lemma eventually_finite (hf : locally_finite f) (x : X) :
+lemma _root_.locally_finite_iff_small_sets :
+  locally_finite f ↔ ∀ x, ∀ᶠ s in (𝓝 x).small_sets, {i | (f i ∩ s).nonempty}.finite :=
+forall_congr $ λ x, iff.symm $ eventually_small_sets' $ λ s t hst ht, ht.subset $
+  λ i hi, hi.mono $ inter_subset_inter_right _ hst
+
+protected lemma eventually_small_sets (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⟩
+locally_finite_iff_small_sets.mp hf x
 
 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)
+let ⟨i, hpi, hi⟩ := hb.small_sets.eventually_iff.mp (hf.eventually_small_sets 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,
@@ -162,3 +154,29 @@ lemma preimage_continuous {g : Y → X} (hf : locally_finite f) (hg : continuous
   in ⟨g ⁻¹' s, hg.continuous_at hsx, hs.subset $ λ i ⟨y, hy⟩, ⟨g y, hy⟩⟩
 
 end locally_finite
+
+@[simp] lemma equiv.locally_finite_comp_iff (e : ι' ≃ ι) :
+  locally_finite (f ∘ e) ↔ locally_finite f :=
+⟨λ h, by simpa only [(∘), e.apply_symm_apply] using h.comp_injective e.symm.injective,
+  λ h, h.comp_injective e.injective⟩
+  
+lemma locally_finite_sum {f : ι ⊕ ι' → set X} :
+  locally_finite f ↔ locally_finite (f ∘ sum.inl) ∧ locally_finite (f ∘ sum.inr) :=
+by simp only [locally_finite_iff_small_sets, ← forall_and_distrib, ← finite_preimage_inl_and_inr,
+  preimage_set_of_eq, (∘), eventually_and]
+
+lemma locally_finite.sum_elim {g : ι' → set X} (hf : locally_finite f) (hg : locally_finite g) :
+  locally_finite (sum.elim f g) :=
+locally_finite_sum.mpr ⟨hf, hg⟩
+
+lemma locally_finite_option {f : option ι → set X} :
+  locally_finite f ↔ locally_finite (f ∘ some) :=
+begin
+  simp only [← (equiv.option_equiv_sum_punit.{u} ι).symm.locally_finite_comp_iff,
+    locally_finite_sum, locally_finite_of_finite, and_true],
+  refl
+end
+
+lemma locally_finite.option_elim (hf : locally_finite f) (s : set X) :
+  locally_finite (option.elim s f) :=
+locally_finite_option.2 hf