mdifferentiable_neg_section — Mathlib

English

If a differentiable section s of a vector bundle is given, then the section sending each base point to the negative of the fiber value, -s, is differentiable as well.

Русский

Если секция s векторного расслоения дифференцируема, то секция, сопоставляющая каждому базисному точке отрицательное значение волокна, -s, также дифференцируема.

LaTeX

$$$ MDifferentiable I (I.prod (modelWithCornersSelf 𝕜 F)) (\x => TotalSpace.mk' F x (- (s x))) \Rightarrow MDifferentiable I (I.prod (modelWithCornersSelf 𝕜 F)) (\x => TotalSpace.mk' F x ( - s x))$$

Lean4

theorem mdifferentiable_neg_section (hs : MDifferentiable I (I.prod 𝓘(𝕜, F)) (fun x ↦ TotalSpace.mk' F x (s x))) :
    MDifferentiable I (I.prod 𝓘(𝕜, F)) (fun x ↦ TotalSpace.mk' F x (-s x)) := fun x₀ ↦
  mdifferentiableAt_neg_section (hs x₀)

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