mdifferentiableWithinAt_sub_section

English

If two sections s and t are differentiable within a set u, then their pointwise difference s - t is differentiable within u.

Русский

Если две секции s и t дифференцируемы на некотором множестве u, то их точечное разность s − t дифференцируема на u.

LaTeX

$$$ MDifferentiableWithinAt I (I.prod 𝓘(𝕜, F)) (\x => TotalSpace.mk' F x ((s - t) x)) u x_0$ given appropriate differentiability of s and t within u$$

Lean4

theorem mdifferentiableWithinAt_sub_section
    (hs : MDifferentiableWithinAt I (I.prod 𝓘(𝕜, F)) (fun x ↦ TotalSpace.mk' F x (s x)) u x₀)
    (ht : MDifferentiableWithinAt I (I.prod 𝓘(𝕜, F)) (fun x ↦ TotalSpace.mk' F x (t x)) u x₀) :
    MDifferentiableWithinAt I (I.prod 𝓘(𝕜, F)) (fun x ↦ TotalSpace.mk' F x ((s - t) x)) u x₀ :=
  by
  rw [sub_eq_add_neg]
  apply mdifferentiableWithinAt_add_section hs <| mdifferentiableWithinAt_neg_section ht

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