sum_section_of_locallyFinite — Mathlib

English

If a single differentiable-at section holds for each i, then the sum over i is differentiable at the point.

Русский

Если для каждого i выполнено дифференцируемое в точке, то сумма по i дифференцируема в точке.

LaTeX

$$$ MDifferentiableAt I (I.prod (modelWithCornersSelf 𝕜 F)) (\x => TotalSpace.mk' F x (s i x)) x0$$

Lean4

/-- The sum of a locally finite collection of sections is differentiable at `x`
if each section is. -/
theorem sum_section_of_locallyFinite (ht : LocallyFinite fun i ↦ {x : B | t i x ≠ 0})
    (ht' : ∀ i, MDifferentiableAt I (I.prod 𝓘(𝕜, F)) (fun x ↦ TotalSpace.mk' F x (t i x)) x₀) :
    MDifferentiableAt I (I.prod 𝓘(𝕜, F)) (fun x ↦ TotalSpace.mk' F x (∑' i, (t i x))) x₀ :=
  by
  simp_rw [← mdifferentiableWithinAt_univ] at ht' ⊢
  exact .sum_section_of_locallyFinite ht ht'

Похожие утверждения