From c5f175456f766f25349c9d4fe2ebfb0b421ff82f Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Wed, 24 Jan 2024 20:28:04 +0100 Subject: [PATCH] Small golf; add contMDiffOn_finprod. --- Mathlib/Geometry/Manifold/Algebra/Monoid.lean | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) diff --git a/Mathlib/Geometry/Manifold/Algebra/Monoid.lean b/Mathlib/Geometry/Manifold/Algebra/Monoid.lean index 62ab02b8d5353e..40259c2b7cf161 100644 --- a/Mathlib/Geometry/Manifold/Algebra/Monoid.lean +++ b/Mathlib/Geometry/Manifold/Algebra/Monoid.lean @@ -349,7 +349,6 @@ theorem contMDiffWithinAt_finset_prod (h : ∀ i ∈ t, ContMDiffWithinAt I' I n #align cont_mdiff_within_at_finset_prod contMDiffWithinAt_finset_prod #align cont_mdiff_within_at_finset_sum contMDiffWithinAt_finset_sum - @[to_additive] theorem ContMDiffAt.prod (h : ∀ i ∈ t, ContMDiffAt I' I n (f i) x₀) : ContMDiffAt I' I n (fun x ↦ ∏ i in t, f i x) x₀ := by @@ -376,6 +375,12 @@ theorem contMDiffAt_finset_prod (h : ∀ i ∈ t, ContMDiffAt I' I n (f i) x) : #align cont_mdiff_at_finset_prod contMDiffAt_finset_prod #align cont_mdiff_at_finset_sum contMDiffAt_finset_sum +@[to_additive] +theorem contMDiffOn_finprod + (lf : LocallyFinite fun i ↦ Function.mulSupport <| f i) (h : ∀ i, ContMDiffOn I' I n (f i) s) : + ContMDiffOn I' I n (fun x ↦ ∏ᶠ i, f i x) s := fun x hx => + contMDiffWithinAt_finprod lf sorry -- fun i hi => h i hi x hx + @[to_additive] theorem contMDiffOn_finset_prod' (h : ∀ i ∈ t, ContMDiffOn I' I n (f i) s) : ContMDiffOn I' I n (∏ i in t, f i) s := fun x hx => @@ -410,10 +415,8 @@ theorem contMDiff_finset_prod (h : ∀ i ∈ t, ContMDiff I' I n (f i)) : @[to_additive] theorem contMDiff_finprod (h : ∀ i, ContMDiff I' I n (f i)) - (hfin : LocallyFinite fun i => mulSupport (f i)) : ContMDiff I' I n fun x => ∏ᶠ i, f i x := by - intro x - rcases finprod_eventually_eq_prod hfin x with ⟨s, hs⟩ - exact (contMDiff_finset_prod (fun i _ => h i) x).congr_of_eventuallyEq hs + (hfin : LocallyFinite fun i => mulSupport (f i)) : ContMDiff I' I n fun x => ∏ᶠ i, f i x := + fun x ↦ contMDiffAt_finprod hfin fun i ↦ h i x #align cont_mdiff_finprod contMDiff_finprod #align cont_mdiff_finsum contMDiff_finsum