mdifferentiable_add_section — Mathlib

English

If a function is MDifferentiable and the base-bounds are satisfied for trivializations, then the fiber-coordinate map under a coordinate-change is differentiable.

Русский

Если функция дифференцируема и базовые условия тривиализации выполнены, то отображение координат волокна при переходе координат дифференцируемо.

LaTeX

$$$\displaystyle MDifferentiable IM IB f \land MDifferentiable IM 𝓘(𝕜, F) g \Rightarrow MDifferentiable IM 𝓘(𝕜, F) (\lambda y. e.coordChange e' (f y) (g y)).$$$

Lean4

theorem mdifferentiable_add_section (hs : MDifferentiable I (I.prod 𝓘(𝕜, F)) (fun x ↦ TotalSpace.mk' F x (s x)))
    (ht : MDifferentiable I (I.prod 𝓘(𝕜, F)) (fun x ↦ TotalSpace.mk' F x (t x))) :
    MDifferentiable I (I.prod 𝓘(𝕜, F)) (fun x ↦ TotalSpace.mk' F x ((s + t) x)) := fun x₀ ↦
  mdifferentiableAt_add_section (hs x₀) (ht x₀)

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