add_section — Mathlib

English

If two smooth sections s and t are ContMDiffOn on a set u, then their sum s+t is ContMDiffOn on u.

Русский

Если две гладкие секции s и t на множестве u, то их сумма s+t гладка на u.

LaTeX

$$$$ \text{If } s,t: M \to V \text{ are ContMDiffOn on } u, \; (s+t) \in \ContMDiffOn I (I.prod ...) n $$$$

Lean4

theorem add_section (hs : ContMDiffOn I (I.prod 𝓘(𝕜, F)) n (fun x ↦ TotalSpace.mk' F x (s x)) u)
    (ht : ContMDiffOn I (I.prod 𝓘(𝕜, F)) n (fun x ↦ TotalSpace.mk' F x (t x)) u) :
    ContMDiffOn I (I.prod 𝓘(𝕜, F)) n (fun x ↦ TotalSpace.mk' F x ((s + t) x)) u := fun x₀ hx₀ ↦
  (hs x₀ hx₀).add_section (ht x₀ hx₀)

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