extDerivWithin_fun_add — Mathlib

English

The extDeriv of the sum of two ω's is the sum of their extDerivs: extDerivWithin((ω1 ⊕ ω2), s, x) = extDerivWithin ω1 s x + extDerivWithin ω2 s x.

Русский

Производная экстерориальная суммы двух ω равна сумме их внешних дифференциалов.

LaTeX

$$$extDerivWithin(ω_1 + ω_2) = extDerivWithin(ω_1) + extDerivWithin(ω_2).$$$

Lean4

theorem extDerivWithin_fun_add (hsx : UniqueDiffWithinAt 𝕜 s x) (hω₁ : DifferentiableWithinAt 𝕜 ω₁ s x)
    (hω₂ : DifferentiableWithinAt 𝕜 ω₂ s x) :
    extDerivWithin (fun x ↦ ω₁ x + ω₂ x) s x = extDerivWithin ω₁ s x + extDerivWithin ω₂ s x :=
  extDerivWithin_add hsx hω₁ hω₂

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