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ω₂