neg_section — Mathlib

English

If a section s is ContMDiffOn I (I.prod 𝓘(𝕜, F)) n on a set u, then the section x ↦ -s(x) is ContMDiffOn I … n on u.

Русский

Если секция s гладкая на множестве u, то секция x ↦ -s(x) тоже гладкая на u.

LaTeX

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

Lean4

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

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