sub_section — Mathlib

English

If s and t are ContMDiffWithinAt on u, then s − t is ContMDiffWithinAt on u.

Русский

Если s и t гладкие в окрестности u, то s − t гладна в той же области.

LaTeX

$$ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) n (fun x ↦ TotalSpace.mk' F x ((s - t) x)) u x0$$

Lean4

theorem sub_section (hs : ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) n (fun x ↦ TotalSpace.mk' F x (s x)) u x₀)
    (ht : ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) n (fun x ↦ TotalSpace.mk' F x (t x)) u x₀) :
    ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) n (fun x ↦ TotalSpace.mk' F x ((s - t) x)) u x₀ :=
  by
  rw [sub_eq_add_neg]
  exact hs.add_section ht.neg_section

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