mdifferentiableAt_sub_section — Mathlib

English

If s and t are differentiable at a point x0, then their difference s - t is differentiable at x0.

Русский

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

LaTeX

$$$ MDifferentiableAt I (I.prod 𝓘(𝕜, F)) (\x => TotalSpace.mk' F x ((s - t) x)) x_0$ from differentiability of s and t at x0$$

Lean4

theorem mdifferentiableAt_sub_section (hs : MDifferentiableAt I (I.prod 𝓘(𝕜, F)) (fun x ↦ TotalSpace.mk' F x (s x)) x₀)
    (ht : MDifferentiableAt I (I.prod 𝓘(𝕜, F)) (fun x ↦ TotalSpace.mk' F x (t x)) x₀) :
    MDifferentiableAt I (I.prod 𝓘(𝕜, F)) (fun x ↦ TotalSpace.mk' F x ((s - t) x)) x₀ :=
  by
  rw [sub_eq_add_neg]
  apply mdifferentiableAt_add_section hs <| mdifferentiableAt_neg_section ht

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