sub_section — Mathlib

English

If s is a ContMDiffAt section, then x ↦ s(x) − t(x) is ContMDiffAt given t and s are ContMDiffAt.

Русский

Если s — секция, гладкая в точке, то s − t гладкая в той же точке, при условии гладкости t.

LaTeX

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

Lean4

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

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