mDifferentiableOn_sub_section — Mathlib

English

If two sections s and t are differentiable on a subset u, then their difference s - t is differentiable on u.

Русский

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

LaTeX

$$$ MDifferentiableOn I (I.prod 𝓘(𝕜, F)) (\x => TotalSpace.mk' F x ((s - t) x)) u$$

Lean4

theorem mDifferentiableOn_sub_section (hs : MDifferentiableOn I (I.prod 𝓘(𝕜, F)) (fun x ↦ TotalSpace.mk' F x (s x)) u)
    (ht : MDifferentiableOn I (I.prod 𝓘(𝕜, F)) (fun x ↦ TotalSpace.mk' F x (t x)) u) :
    MDifferentiableOn I (I.prod 𝓘(𝕜, F)) (fun x ↦ TotalSpace.mk' F x ((s - t) x)) u := fun x₀ hx₀ ↦
  mdifferentiableWithinAt_sub_section (hs x₀ hx₀) (ht x₀ hx₀)

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