neg_section — Mathlib

English

If s and t are C^n sections, then the subtraction s − t is a C^n section.

Русский

Если s и t — секции порядка n, то секция s − t гладна до порядка n.

LaTeX

$$$s,t \\in \\Gamma^{(n)}(M,V) \\Rightarrow s-t \\in \\Gamma^{(n)}(M,V)$$$

Lean4

theorem neg_section (hs : ContMDiff I (I.prod 𝓘(𝕜, F)) n (fun x ↦ TotalSpace.mk' F x (s x))) :
    ContMDiff I (I.prod 𝓘(𝕜, F)) n (fun x ↦ TotalSpace.mk' F x (-s x)) := fun x₀ ↦ (hs x₀).neg_section

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