From ac0ad1e804edff1e62245628407395de22e72302 Mon Sep 17 00:00:00 2001 From: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Tue, 12 Sep 2023 22:27:39 +0000 Subject: [PATCH] chore: tidy various files (#7081) --- Mathlib/Algebra/BigOperators/Finprod.lean | 54 ++++---- Mathlib/Analysis/Convex/Combination.lean | 2 +- .../SpecialFunctions/Trigonometric/Basic.lean | 125 +++++++++--------- Mathlib/Geometry/Manifold/BumpFunction.lean | 6 +- Mathlib/Order/Filter/Bases.lean | 27 ++-- .../MetricSpace/HausdorffDistance.lean | 4 +- 6 files changed, 108 insertions(+), 110 deletions(-) diff --git a/Mathlib/Algebra/BigOperators/Finprod.lean b/Mathlib/Algebra/BigOperators/Finprod.lean index 206d7b56eca3b..66cd2ae32d77b 100644 --- a/Mathlib/Algebra/BigOperators/Finprod.lean +++ b/Mathlib/Algebra/BigOperators/Finprod.lean @@ -47,11 +47,11 @@ This notation works for functions `f : p → M`, where `p : Prop`, so the follow ## Implementation notes -`Finsum` and `Finprod` is "yet another way of doing finite sums and products in Lean". However +`finsum` and `finprod` is "yet another way of doing finite sums and products in Lean". However experiments in the wild (e.g. with matroids) indicate that it is a helpful approach in settings where the user is not interested in computability and wants to do reasoning without running into typeclass diamonds caused by the constructive finiteness used in definitions such as `Finset` and -`Fintype`. By sticking solely to `Set.finite` we avoid these problems. We are aware that there are +`Fintype`. By sticking solely to `Set.Finite` we avoid these problems. We are aware that there are other solutions but for beginner mathematicians this approach is easier in practice. Another application is the construction of a partition of unity from a collection of “bump” @@ -171,29 +171,29 @@ notation3"∏ᶠ "(...)", "r:67:(scoped f => finprod f) => r -- (finprod (α := $t) fun $h => $p)))) @[to_additive] -theorem finprod_eq_prod_pLift_of_mulSupport_toFinset_subset {f : α → M} +theorem finprod_eq_prod_plift_of_mulSupport_toFinset_subset {f : α → M} (hf : (mulSupport (f ∘ PLift.down)).Finite) {s : Finset (PLift α)} (hs : hf.toFinset ⊆ s) : ∏ᶠ i, f i = ∏ i in s, f i.down := by rw [finprod, dif_pos] refine' Finset.prod_subset hs fun x _ hxf => _ rwa [hf.mem_toFinset, nmem_mulSupport] at hxf -#align finprod_eq_prod_plift_of_mul_support_to_finset_subset finprod_eq_prod_pLift_of_mulSupport_toFinset_subset -#align finsum_eq_sum_plift_of_support_to_finset_subset finsum_eq_sum_pLift_of_support_toFinset_subset +#align finprod_eq_prod_plift_of_mul_support_to_finset_subset finprod_eq_prod_plift_of_mulSupport_toFinset_subset +#align finsum_eq_sum_plift_of_support_to_finset_subset finsum_eq_sum_plift_of_support_toFinset_subset @[to_additive] -theorem finprod_eq_prod_pLift_of_mulSupport_subset {f : α → M} {s : Finset (PLift α)} +theorem finprod_eq_prod_plift_of_mulSupport_subset {f : α → M} {s : Finset (PLift α)} (hs : mulSupport (f ∘ PLift.down) ⊆ s) : ∏ᶠ i, f i = ∏ i in s, f i.down := - finprod_eq_prod_pLift_of_mulSupport_toFinset_subset (s.finite_toSet.subset hs) fun x hx => by + finprod_eq_prod_plift_of_mulSupport_toFinset_subset (s.finite_toSet.subset hs) fun x hx => by rw [Finite.mem_toFinset] at hx exact hs hx -#align finprod_eq_prod_plift_of_mul_support_subset finprod_eq_prod_pLift_of_mulSupport_subset -#align finsum_eq_sum_plift_of_support_subset finsum_eq_sum_pLift_of_support_subset +#align finprod_eq_prod_plift_of_mul_support_subset finprod_eq_prod_plift_of_mulSupport_subset +#align finsum_eq_sum_plift_of_support_subset finsum_eq_sum_plift_of_support_subset @[to_additive (attr := simp)] theorem finprod_one : (∏ᶠ _ : α, (1 : M)) = 1 := by have : (mulSupport fun x : PLift α => (fun _ => 1 : α → M) x.down) ⊆ (∅ : Finset (PLift α)) := fun x h => by simp at h - rw [finprod_eq_prod_pLift_of_mulSupport_subset this, Finset.prod_empty] + rw [finprod_eq_prod_plift_of_mulSupport_subset this, Finset.prod_empty] #align finprod_one finprod_one #align finsum_zero finsum_zero @@ -212,13 +212,13 @@ theorem finprod_false (f : False → M) : ∏ᶠ i, f i = 1 := #align finsum_false finsum_false @[to_additive] -theorem finprod_eq_single (f : α → M) (a : α) (ha : ∀ (x) (_ : x ≠ a), f x = 1) : +theorem finprod_eq_single (f : α → M) (a : α) (ha : ∀ x, x ≠ a → f x = 1) : ∏ᶠ x, f x = f a := by have : mulSupport (f ∘ PLift.down) ⊆ ({PLift.up a} : Finset (PLift α)) := by intro x contrapose simpa [PLift.eq_up_iff_down_eq] using ha x.down - rw [finprod_eq_prod_pLift_of_mulSupport_subset this, Finset.prod_singleton] + rw [finprod_eq_prod_plift_of_mulSupport_subset this, Finset.prod_singleton] #align finprod_eq_single finprod_eq_single #align finsum_eq_single finsum_eq_single @@ -291,26 +291,26 @@ theorem one_le_finprod' {M : Type*} [OrderedCommMonoid M] {f : α → M} (hf : #align finsum_nonneg finsum_nonneg @[to_additive] -theorem MonoidHom.map_finprod_pLift (f : M →* N) (g : α → M) +theorem MonoidHom.map_finprod_plift (f : M →* N) (g : α → M) (h : (mulSupport <| g ∘ PLift.down).Finite) : f (∏ᶠ x, g x) = ∏ᶠ x, f (g x) := by - rw [finprod_eq_prod_pLift_of_mulSupport_subset h.coe_toFinset.ge, - finprod_eq_prod_pLift_of_mulSupport_subset, f.map_prod] + rw [finprod_eq_prod_plift_of_mulSupport_subset h.coe_toFinset.ge, + finprod_eq_prod_plift_of_mulSupport_subset, f.map_prod] rw [h.coe_toFinset] exact mulSupport_comp_subset f.map_one (g ∘ PLift.down) -#align monoid_hom.map_finprod_plift MonoidHom.map_finprod_pLift -#align add_monoid_hom.map_finsum_plift AddMonoidHom.map_finsum_pLift +#align monoid_hom.map_finprod_plift MonoidHom.map_finprod_plift +#align add_monoid_hom.map_finsum_plift AddMonoidHom.map_finsum_plift @[to_additive] theorem MonoidHom.map_finprod_Prop {p : Prop} (f : M →* N) (g : p → M) : f (∏ᶠ x, g x) = ∏ᶠ x, f (g x) := - f.map_finprod_pLift g (Set.toFinite _) + f.map_finprod_plift g (Set.toFinite _) #align monoid_hom.map_finprod_Prop MonoidHom.map_finprod_Prop #align add_monoid_hom.map_finsum_Prop AddMonoidHom.map_finsum_Prop @[to_additive] theorem MonoidHom.map_finprod_of_preimage_one (f : M →* N) (hf : ∀ x, f x = 1 → x = 1) (g : α → M) : f (∏ᶠ i, g i) = ∏ᶠ i, f (g i) := by - by_cases hg : (mulSupport <| g ∘ PLift.down).Finite; · exact f.map_finprod_pLift g hg + by_cases hg : (mulSupport <| g ∘ PLift.down).Finite; · exact f.map_finprod_plift g hg rw [finprod, dif_neg, f.map_one, finprod, dif_neg] exacts [Infinite.mono (fun x hx => mt (hf (g x.down)) hx) hg, hg] #align monoid_hom.map_finprod_of_preimage_one MonoidHom.map_finprod_of_preimage_one @@ -333,16 +333,18 @@ theorem MulEquiv.map_finprod (g : M ≃* N) (f : α → M) : g (∏ᶠ i, f i) = infinite. For a more usual version assuming `(support f).Finite` instead, see `finsum_smul'`. -/ theorem finsum_smul {R M : Type*} [Ring R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] (f : ι → R) (x : M) : (∑ᶠ i, f i) • x = ∑ᶠ i, f i • x := by - rcases eq_or_ne x 0 with (rfl | hx); · simp - exact ((smulAddHom R M).flip x).map_finsum_of_injective (smul_left_injective R hx) _ + rcases eq_or_ne x 0 with (rfl | hx) + · simp + · exact ((smulAddHom R M).flip x).map_finsum_of_injective (smul_left_injective R hx) _ #align finsum_smul finsum_smul /-- The `NoZeroSMulDivisors` makes sure that the result holds even when the support of `f` is infinite. For a more usual version assuming `(support f).Finite` instead, see `smul_finsum'`. -/ theorem smul_finsum {R M : Type*} [Ring R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] (c : R) (f : ι → M) : (c • ∑ᶠ i, f i) = ∑ᶠ i, c • f i := by - rcases eq_or_ne c 0 with (rfl | hc); · simp - exact (smulAddHom R M c).map_finsum_of_injective (smul_right_injective M hc) _ + rcases eq_or_ne c 0 with (rfl | hc) + · simp + · exact (smulAddHom R M c).map_finsum_of_injective (smul_right_injective M hc) _ #align smul_finsum smul_finsum @[to_additive] @@ -388,7 +390,7 @@ theorem finprod_eq_prod_of_mulSupport_subset (f : α → M) {s : Finset α} (h : have : mulSupport (f ∘ PLift.down) ⊆ s.map Equiv.plift.symm.toEmbedding := by rw [A, Finset.coe_map] exact image_subset _ h - rw [finprod_eq_prod_pLift_of_mulSupport_subset this] + rw [finprod_eq_prod_plift_of_mulSupport_subset this] simp only [Finset.prod_map, Equiv.coe_toEmbedding] congr #align finprod_eq_prod_of_mul_support_subset finprod_eq_prod_of_mulSupport_subset @@ -619,7 +621,7 @@ theorem finprod_mul_distrib (hf : (mulSupport f).Finite) (hg : (mulSupport g).Fi mem_union, mem_mulSupport] intro x contrapose! - rintro ⟨hf,hg⟩ + rintro ⟨hf, hg⟩ simp [hf, hg] #align finprod_mul_distrib finprod_mul_distrib #align finsum_add_distrib finsum_add_distrib @@ -689,7 +691,7 @@ theorem finprod_mem_mul_distrib (hs : s.Finite) : @[to_additive] theorem MonoidHom.map_finprod {f : α → M} (g : M →* N) (hf : (mulSupport f).Finite) : g (∏ᶠ i, f i) = ∏ᶠ i, g (f i) := - g.map_finprod_pLift f <| hf.preimage <| Equiv.plift.injective.injOn _ + g.map_finprod_plift f <| hf.preimage <| Equiv.plift.injective.injOn _ #align monoid_hom.map_finprod MonoidHom.map_finprod #align add_monoid_hom.map_finsum AddMonoidHom.map_finsum diff --git a/Mathlib/Analysis/Convex/Combination.lean b/Mathlib/Analysis/Convex/Combination.lean index b95499f4e25da..7175fb01e7056 100644 --- a/Mathlib/Analysis/Convex/Combination.lean +++ b/Mathlib/Analysis/Convex/Combination.lean @@ -192,7 +192,7 @@ theorem Convex.finsum_mem {ι : Sort*} {w : ι → R} {z : ι → E} {s : Set E} exact zero_ne_one h₁ have hsub : support ((fun i => w i • z i) ∘ PLift.down) ⊆ hfin_w.toFinset := (support_smul_subset_left _ _).trans hfin_w.coe_toFinset.ge - rw [finsum_eq_sum_pLift_of_support_subset hsub] + rw [finsum_eq_sum_plift_of_support_subset hsub] refine' hs.sum_mem (fun _ _ => h₀ _) _ fun i hi => hz _ _ · rwa [finsum, dif_pos hfin_w] at h₁ · rwa [hfin_w.mem_toFinset] at hi diff --git a/Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean b/Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean index 98a46cc6e67df..1f29b8e96703c 100644 --- a/Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean +++ b/Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean @@ -504,15 +504,12 @@ theorem cos_eq_sqrt_one_sub_sin_sq {x : ℝ} (hl : -(π / 2) ≤ x) (hu : x ≤ #align real.cos_eq_sqrt_one_sub_sin_sq Real.cos_eq_sqrt_one_sub_sin_sq theorem sin_eq_zero_iff_of_lt_of_lt {x : ℝ} (hx₁ : -π < x) (hx₂ : x < π) : sin x = 0 ↔ x = 0 := - ⟨fun h => le_antisymm (le_of_not_gt fun h0 => lt_irrefl (0 : ℝ) <| - calc - 0 < sin x := sin_pos_of_pos_of_lt_pi h0 hx₂ - _ = 0 := h) - (le_of_not_gt fun h0 => lt_irrefl (0 : ℝ) <| - calc - 0 = sin x := h.symm - _ < 0 := sin_neg_of_neg_of_neg_pi_lt h0 hx₁), - fun h => by simp [h]⟩ + ⟨fun h => by + contrapose! h + cases h.lt_or_lt with + | inl h0 => exact (sin_neg_of_neg_of_neg_pi_lt h0 hx₁).ne + | inr h0 => exact (sin_pos_of_pos_of_lt_pi h0 hx₂).ne', + fun h => by simp [h]⟩ #align real.sin_eq_zero_iff_of_lt_of_lt Real.sin_eq_zero_iff_of_lt_of_lt theorem sin_eq_zero_iff {x : ℝ} : sin x = 0 ↔ ∃ n : ℤ, (n : ℝ) * π = x := @@ -736,24 +733,23 @@ theorem cos_pi_over_two_pow : ∀ n : ℕ, cos (π / 2 ^ (n + 1)) = sqrtTwoAddSe | 0 => by simp | n + 1 => by have : (2 : ℝ) ≠ 0 := two_ne_zero - symm; rw [div_eq_iff_mul_eq this]; symm - rw [sqrtTwoAddSeries, sqrt_eq_iff_sq_eq, mul_pow, cos_sq, ← mul_div_assoc, Nat.add_succ, - pow_succ, mul_div_mul_left _ _ this, cos_pi_over_two_pow _, add_mul] - congr; · norm_num - rw [mul_comm, sq, mul_assoc, ← mul_div_assoc, mul_div_cancel_left, ← mul_div_assoc, - mul_div_cancel_left] <;> - try exact this - apply add_nonneg; norm_num; apply sqrtTwoAddSeries_zero_nonneg; norm_num - apply le_of_lt; apply cos_pos_of_mem_Ioo ⟨_, _⟩ + rw [eq_div_iff_mul_eq this, eq_comm, sqrtTwoAddSeries, sqrt_eq_iff_sq_eq, mul_pow, cos_sq, + ← mul_div_assoc, pow_succ, mul_div_mul_left _ _ this, cos_pi_over_two_pow _, add_mul] + · congr + · norm_num + · rw [mul_comm, sq, mul_assoc, ← mul_div_assoc, mul_div_cancel_left _ this, ← mul_div_assoc, + mul_div_cancel_left _ this] + · exact add_nonneg two_pos.le (sqrtTwoAddSeries_zero_nonneg _) + refine le_of_lt <| mul_pos (cos_pos_of_mem_Ioo ⟨?_, ?_⟩) two_pos · trans (0 : ℝ) - rw [neg_lt_zero] - apply pi_div_two_pos - apply div_pos pi_pos - apply pow_pos - norm_num - apply div_lt_div' (le_refl π) _ pi_pos _ + · rw [neg_lt_zero] + exact pi_div_two_pos + · exact div_pos pi_pos <| pow_pos two_pos _ + apply div_lt_div' (le_refl π) _ pi_pos two_pos refine' lt_of_le_of_lt (le_of_eq (pow_one _).symm) _ - apply pow_lt_pow; norm_num; apply Nat.succ_lt_succ; apply Nat.succ_pos; all_goals norm_num + apply pow_lt_pow + · norm_num + · exact Nat.succ_lt_succ n.succ_pos #align real.cos_pi_over_two_pow Real.cos_pi_over_two_pow theorem sin_sq_pi_over_two_pow (n : ℕ) : @@ -764,90 +760,92 @@ theorem sin_sq_pi_over_two_pow (n : ℕ) : theorem sin_sq_pi_over_two_pow_succ (n : ℕ) : sin (π / 2 ^ (n + 2)) ^ 2 = 1 / 2 - sqrtTwoAddSeries 0 n / 4 := by rw [sin_sq_pi_over_two_pow, sqrtTwoAddSeries, div_pow, sq_sqrt, add_div, ← sub_sub] - congr; norm_num; norm_num; apply add_nonneg; norm_num; apply sqrtTwoAddSeries_zero_nonneg + congr + · norm_num + · norm_num + · exact add_nonneg two_pos.le (sqrtTwoAddSeries_zero_nonneg _) #align real.sin_sq_pi_over_two_pow_succ Real.sin_sq_pi_over_two_pow_succ @[simp] theorem sin_pi_over_two_pow_succ (n : ℕ) : sin (π / 2 ^ (n + 2)) = sqrt (2 - sqrtTwoAddSeries 0 n) / 2 := by - symm; rw [div_eq_iff_mul_eq]; symm - rw [sqrt_eq_iff_sq_eq, mul_pow, sin_sq_pi_over_two_pow_succ, sub_mul] + rw [eq_div_iff_mul_eq two_ne_zero, eq_comm, sqrt_eq_iff_sq_eq, mul_pow, + sin_sq_pi_over_two_pow_succ, sub_mul] · congr <;> norm_num · rw [sub_nonneg] - apply le_of_lt - apply sqrtTwoAddSeries_lt_two - apply le_of_lt; apply mul_pos; apply sin_pos_of_pos_of_lt_pi - · apply div_pos pi_pos - apply pow_pos - norm_num - refine' lt_of_lt_of_le _ (le_of_eq (div_one _)); rw [div_lt_div_left] + exact (sqrtTwoAddSeries_lt_two _).le + refine le_of_lt <| mul_pos (sin_pos_of_pos_of_lt_pi ?_ ?_) two_pos + · exact div_pos pi_pos <| pow_pos two_pos _ + refine' lt_of_lt_of_le _ (le_of_eq (div_one _)) + rw [div_lt_div_left pi_pos (pow_pos two_pos _) one_pos] refine' lt_of_le_of_lt (le_of_eq (pow_zero 2).symm) _ - apply pow_lt_pow; norm_num; apply Nat.succ_pos; apply pi_pos - apply pow_pos; all_goals norm_num + apply pow_lt_pow + · norm_num + · apply Nat.succ_pos #align real.sin_pi_over_two_pow_succ Real.sin_pi_over_two_pow_succ @[simp] theorem cos_pi_div_four : cos (π / 4) = sqrt 2 / 2 := by trans cos (π / 2 ^ 2) - congr - norm_num - simp + · congr + norm_num + · simp #align real.cos_pi_div_four Real.cos_pi_div_four @[simp] theorem sin_pi_div_four : sin (π / 4) = sqrt 2 / 2 := by trans sin (π / 2 ^ 2) - congr - norm_num - simp + · congr + norm_num + · simp #align real.sin_pi_div_four Real.sin_pi_div_four @[simp] theorem cos_pi_div_eight : cos (π / 8) = sqrt (2 + sqrt 2) / 2 := by trans cos (π / 2 ^ 3) - congr - norm_num - simp + · congr + norm_num + · simp #align real.cos_pi_div_eight Real.cos_pi_div_eight @[simp] theorem sin_pi_div_eight : sin (π / 8) = sqrt (2 - sqrt 2) / 2 := by trans sin (π / 2 ^ 3) - congr - norm_num - simp + · congr + norm_num + · simp #align real.sin_pi_div_eight Real.sin_pi_div_eight @[simp] theorem cos_pi_div_sixteen : cos (π / 16) = sqrt (2 + sqrt (2 + sqrt 2)) / 2 := by trans cos (π / 2 ^ 4) - congr - norm_num - simp + · congr + norm_num + · simp #align real.cos_pi_div_sixteen Real.cos_pi_div_sixteen @[simp] theorem sin_pi_div_sixteen : sin (π / 16) = sqrt (2 - sqrt (2 + sqrt 2)) / 2 := by trans sin (π / 2 ^ 4) - congr - norm_num - simp + · congr + norm_num + · simp #align real.sin_pi_div_sixteen Real.sin_pi_div_sixteen @[simp] theorem cos_pi_div_thirty_two : cos (π / 32) = sqrt (2 + sqrt (2 + sqrt (2 + sqrt 2))) / 2 := by trans cos (π / 2 ^ 5) - congr - norm_num - simp + · congr + norm_num + · simp #align real.cos_pi_div_thirty_two Real.cos_pi_div_thirty_two @[simp] theorem sin_pi_div_thirty_two : sin (π / 32) = sqrt (2 - sqrt (2 + sqrt (2 + sqrt 2))) / 2 := by trans sin (π / 2 ^ 5) - congr - norm_num - simp + · congr + norm_num + · simp #align real.sin_pi_div_thirty_two Real.sin_pi_div_thirty_two -- This section is also a convenient location for other explicit values of `sin` and `cos`. @@ -862,7 +860,7 @@ theorem cos_pi_div_three : cos (π / 3) = 1 / 2 := by cases' mul_eq_zero.mp h₁ with h h · linarith [pow_eq_zero h] · have : cos π < cos (π / 3) := by - refine' cos_lt_cos_of_nonneg_of_le_pi _ rfl.ge _ <;> linarith [pi_pos] + refine' cos_lt_cos_of_nonneg_of_le_pi _ le_rfl _ <;> linarith [pi_pos] linarith [cos_pi] #align real.cos_pi_div_three Real.cos_pi_div_three @@ -882,8 +880,7 @@ theorem sq_cos_pi_div_six : cos (π / 6) ^ 2 = 3 / 4 := by @[simp] theorem cos_pi_div_six : cos (π / 6) = sqrt 3 / 2 := by suffices sqrt 3 = cos (π / 6) * 2 by - field_simp [(by norm_num : 0 ≠ 2)] - exact this.symm + field_simp [(by norm_num : 0 ≠ 2), ← this] rw [sqrt_eq_iff_sq_eq] · have h1 := (mul_right_inj' (by norm_num : (4 : ℝ) ≠ 0)).mpr sq_cos_pi_div_six rw [← sub_eq_zero] at h1 ⊢ diff --git a/Mathlib/Geometry/Manifold/BumpFunction.lean b/Mathlib/Geometry/Manifold/BumpFunction.lean index ec7a4bb01fa88..819e014129dbc 100644 --- a/Mathlib/Geometry/Manifold/BumpFunction.lean +++ b/Mathlib/Geometry/Manifold/BumpFunction.lean @@ -204,7 +204,7 @@ theorem nhdsWithin_range_basis : (𝓝[range I] extChartAt I c c).HasBasis (fun _ : SmoothBumpFunction I c => True) fun f => closedBall (extChartAt I c c) f.rOut ∩ range I := by refine' ((nhdsWithin_hasBasis nhds_basis_closedBall _).restrict_subset - (extChartAt_target_mem_nhdsWithin _ _)).to_has_basis' _ _ + (extChartAt_target_mem_nhdsWithin _ _)).to_hasBasis' _ _ · rintro R ⟨hR0, hsub⟩ exact ⟨⟨⟨R / 2, R, half_pos hR0, half_lt_self hR0⟩, hsub⟩, trivial, Subset.rfl⟩ · exact fun f _ => inter_mem (mem_nhdsWithin_of_mem_nhds <| closedBall_mem_nhds _ f.rOut_pos) @@ -293,7 +293,7 @@ theorem nhds_basis_tsupport : (extChartAt I c).symm '' (closedBall (extChartAt I c c) f.rOut ∩ range I) := by rw [← map_extChartAt_symm_nhdsWithin_range I c] exact nhdsWithin_range_basis.map _ - refine' this.to_has_basis' (fun f _ => ⟨f, trivial, f.tsupport_subset_symm_image_closedBall⟩) + refine' this.to_hasBasis' (fun f _ => ⟨f, trivial, f.tsupport_subset_symm_image_closedBall⟩) fun f _ => f.tsupport_mem_nhds #align smooth_bump_function.nhds_basis_tsupport SmoothBumpFunction.nhds_basis_tsupport @@ -305,7 +305,7 @@ neighborhood of `c` and each neighborhood of `c` includes `support f` for some `f : SmoothBumpFunction I c` such that `tsupport f ⊆ s`. -/ theorem nhds_basis_support {s : Set M} (hs : s ∈ 𝓝 c) : (𝓝 c).HasBasis (fun f : SmoothBumpFunction I c => tsupport f ⊆ s) fun f => support f := - ((nhds_basis_tsupport I c).restrict_subset hs).to_has_basis' + ((nhds_basis_tsupport I c).restrict_subset hs).to_hasBasis' (fun f hf => ⟨f, hf.2, subset_closure⟩) fun f _ => f.support_mem_nhds #align smooth_bump_function.nhds_basis_support SmoothBumpFunction.nhds_basis_support diff --git a/Mathlib/Order/Filter/Bases.lean b/Mathlib/Order/Filter/Bases.lean index c5be822ca3cae..121f8c7f2da75 100644 --- a/Mathlib/Order/Filter/Bases.lean +++ b/Mathlib/Order/Filter/Bases.lean @@ -21,7 +21,7 @@ to `B.filter` if and only if it contains an element of `B`. Given an indexing type `ι`, a predicate `p : ι → Prop`, and a map `s : ι → Set α`, the proposition `h : Filter.IsBasis p s` makes sure the range of `s` bounded by `p` -(ie. `s '' setOf p`) defines a filter basis `h.filter_basis`. +(ie. `s '' setOf p`) defines a filter basis `h.filterBasis`. If one already has a filter `l` on `α`, `Filter.HasBasis l p s` (where `p : ι → Prop` and `s : ι → Set α` as above) means that a set belongs to `l` if and @@ -54,9 +54,9 @@ and consequences are derived. `l ≤ l'` in terms of bases. * `Filter.HasBasis.tendsto_right_iff`, `Filter.HasBasis.tendsto_left_iff`, - `Filter.HasBasis.tendsto_iff` : restate `tendsto f l l'` in terms of bases. + `Filter.HasBasis.tendsto_iff` : restate `Tendsto f l l'` in terms of bases. -* `is_countably_generated_iff_exists_antitone_basis` : proves a filter is countably generated if and +* `isCountablyGenerated_iff_exists_antitone_basis` : proves a filter is countably generated if and only if it admits a basis parametrized by a decreasing sequence of sets indexed by `ℕ`. * `tendsto_iff_seq_tendsto ` : an abstract version of "sequentially continuous implies continuous". @@ -112,7 +112,7 @@ instance {α : Type*} : Membership (Set α) (FilterBasis α) := @[simp] theorem FilterBasis.mem_sets {s : Set α} {B : FilterBasis α} : s ∈ B.sets ↔ s ∈ B := Iff.rfl --- For illustration purposes, the filter basis defining (at_top : filter ℕ) +-- For illustration purposes, the filter basis defining `(atTop : Filter ℕ)` instance : Inhabited (FilterBasis ℕ) := ⟨{ sets := range Ici nonempty := ⟨Ici 0, mem_range_self 0⟩ @@ -163,8 +163,7 @@ end Filter namespace FilterBasis /-- The filter associated to a filter basis. -/ -protected def filter (B : FilterBasis α) : Filter α - where +protected def filter (B : FilterBasis α) : Filter α where sets := { s | ∃ t ∈ B, t ⊆ s } univ_sets := B.nonempty.imp <| fun s s_in => ⟨s_in, s.subset_univ⟩ sets_of_superset := fun ⟨s, s_in, h⟩ hxy => ⟨s, s_in, Set.Subset.trans h hxy⟩ @@ -314,7 +313,7 @@ theorem HasBasis.set_index_subset (h : l.HasBasis p s) (ht : t ∈ l) : s (h.ind theorem HasBasis.isBasis (h : l.HasBasis p s) : IsBasis p s where nonempty := h.ex_mem - inter := fun hi hj => by + inter hi hj := by simpa only [h.mem_iff] using inter_mem (h.mem_of_mem hi) (h.mem_of_mem hj) #align filter.has_basis.is_basis Filter.HasBasis.isBasis @@ -342,24 +341,24 @@ protected theorem _root_.FilterBasis.hasBasis (B : FilterBasis α) : ⟨fun _ => B.mem_filter_iff⟩ #align filter_basis.has_basis FilterBasis.hasBasis -theorem HasBasis.to_has_basis' (hl : l.HasBasis p s) (h : ∀ i, p i → ∃ i', p' i' ∧ s' i' ⊆ s i) +theorem HasBasis.to_hasBasis' (hl : l.HasBasis p s) (h : ∀ i, p i → ∃ i', p' i' ∧ s' i' ⊆ s i) (h' : ∀ i', p' i' → s' i' ∈ l) : l.HasBasis p' s' := by refine' ⟨fun t => ⟨fun ht => _, fun ⟨i', hi', ht⟩ => mem_of_superset (h' i' hi') ht⟩⟩ rcases hl.mem_iff.1 ht with ⟨i, hi, ht⟩ rcases h i hi with ⟨i', hi', hs's⟩ exact ⟨i', hi', hs's.trans ht⟩ -#align filter.has_basis.to_has_basis' Filter.HasBasis.to_has_basis' +#align filter.has_basis.to_has_basis' Filter.HasBasis.to_hasBasis' theorem HasBasis.to_hasBasis (hl : l.HasBasis p s) (h : ∀ i, p i → ∃ i', p' i' ∧ s' i' ⊆ s i) (h' : ∀ i', p' i' → ∃ i, p i ∧ s i ⊆ s' i') : l.HasBasis p' s' := - hl.to_has_basis' h fun i' hi' => + hl.to_hasBasis' h fun i' hi' => let ⟨i, hi, hss'⟩ := h' i' hi' hl.mem_iff.2 ⟨i, hi, hss'⟩ #align filter.has_basis.to_has_basis Filter.HasBasis.to_hasBasis theorem HasBasis.to_subset (hl : l.HasBasis p s) {t : ι → Set α} (h : ∀ i, p i → t i ⊆ s i) (ht : ∀ i, p i → t i ∈ l) : l.HasBasis p t := - hl.to_has_basis' (fun i hi => ⟨i, hi, h i hi⟩) ht + hl.to_hasBasis' (fun i hi => ⟨i, hi, h i hi⟩) ht #align filter.has_basis.to_subset Filter.HasBasis.to_subset theorem HasBasis.eventually_iff (hl : l.HasBasis p s) {q : α → Prop} : @@ -552,7 +551,7 @@ theorem hasBasis_biInf_of_directed' {ι : Type*} {ι' : ι → Sort _} {dom : Se rw [mem_biInf_of_directed h hdom, Sigma.exists] refine' exists_congr fun i => ⟨_, _⟩ · rintro ⟨hi, hti⟩ - rcases(hl i hi).mem_iff.mp hti with ⟨b, hb, hbt⟩ + rcases (hl i hi).mem_iff.mp hti with ⟨b, hb, hbt⟩ exact ⟨b, ⟨hi, hb⟩, hbt⟩ · rintro ⟨b, ⟨hi, hb⟩, hibt⟩ exact ⟨hi, (hl i hi).mem_iff.mpr ⟨b, hb, hibt⟩⟩ @@ -567,7 +566,7 @@ theorem hasBasis_biInf_of_directed {ι : Type*} {ι' : Sort _} {dom : Set ι} (h rw [mem_biInf_of_directed h hdom, Prod.exists] refine' exists_congr fun i => ⟨_, _⟩ · rintro ⟨hi, hti⟩ - rcases(hl i hi).mem_iff.mp hti with ⟨b, hb, hbt⟩ + rcases (hl i hi).mem_iff.mp hti with ⟨b, hb, hbt⟩ exact ⟨b, ⟨hi, hb⟩, hbt⟩ · rintro ⟨b, ⟨hi, hb⟩, hibt⟩ exact ⟨hi, (hl i hi).mem_iff.mpr ⟨b, hb, hibt⟩⟩ @@ -1002,7 +1001,7 @@ structure CountableFilterBasis (α : Type*) extends FilterBasis α where countable : sets.Countable #align filter.countable_filter_basis Filter.CountableFilterBasis --- For illustration purposes, the countable filter basis defining `(AtTop : Filter ℕ)` +-- For illustration purposes, the countable filter basis defining `(atTop : Filter ℕ)` instance Nat.inhabitedCountableFilterBasis : Inhabited (CountableFilterBasis ℕ) := ⟨⟨default, countable_range fun n => Ici n⟩⟩ #align filter.nat.inhabited_countable_filter_basis Filter.Nat.inhabitedCountableFilterBasis diff --git a/Mathlib/Topology/MetricSpace/HausdorffDistance.lean b/Mathlib/Topology/MetricSpace/HausdorffDistance.lean index 4de348aa2254f..64c0ffb863add 100644 --- a/Mathlib/Topology/MetricSpace/HausdorffDistance.lean +++ b/Mathlib/Topology/MetricSpace/HausdorffDistance.lean @@ -1311,13 +1311,13 @@ theorem _root_.IsCompact.exists_thickening_subset_open (hs : IsCompact s) (ht : theorem hasBasis_nhdsSet_thickening {K : Set α} (hK : IsCompact K) : (𝓝ˢ K).HasBasis (fun δ : ℝ => 0 < δ) fun δ => thickening δ K := - (hasBasis_nhdsSet K).to_has_basis' (fun _U hU => hK.exists_thickening_subset_open hU.1 hU.2) + (hasBasis_nhdsSet K).to_hasBasis' (fun _U hU => hK.exists_thickening_subset_open hU.1 hU.2) fun _ => thickening_mem_nhdsSet K #align metric.has_basis_nhds_set_thickening Metric.hasBasis_nhdsSet_thickening theorem hasBasis_nhdsSet_cthickening {K : Set α} (hK : IsCompact K) : (𝓝ˢ K).HasBasis (fun δ : ℝ => 0 < δ) fun δ => cthickening δ K := - (hasBasis_nhdsSet K).to_has_basis' (fun _U hU => hK.exists_cthickening_subset_open hU.1 hU.2) + (hasBasis_nhdsSet K).to_hasBasis' (fun _U hU => hK.exists_cthickening_subset_open hU.1 hU.2) fun _ => cthickening_mem_nhdsSet K #align metric.has_basis_nhds_set_cthickening Metric.hasBasis_nhdsSet_cthickening