add_section — Mathlib

English

Let s and t be C^n (ContMDiff) sections of a vector bundle. Then their sum 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 add_section (hs : ContMDiff I (I.prod 𝓘(𝕜, F)) n (fun x ↦ TotalSpace.mk' F x (s x)))
    (ht : ContMDiff I (I.prod 𝓘(𝕜, F)) n (fun x ↦ TotalSpace.mk' F x (t x))) :
    ContMDiff I (I.prod 𝓘(𝕜, F)) n (fun x ↦ TotalSpace.mk' F x ((s + t) x)) := fun x₀ ↦ (hs x₀).add_section (ht x₀)

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