mdifferentiableWithinAt_proj — Mathlib

English

The zero section of a vector bundle is differentiable on any set in the MDifferentiable sense.

Русский

Нулевая секция векторного расслоения дифференцируема на любом множестве в смысле MDifferentiable.

LaTeX

$$$$MDifferentiableOn IB (IB.prod 𝓘(\mathbb{k}, F)) (zeroSection F E) t.$$$$

Lean4

theorem mdifferentiableWithinAt_proj {s : Set (TotalSpace F E)} {p : TotalSpace F E} :
    MDifferentiableWithinAt (IB.prod 𝓘(𝕜, F)) IB (π F E) s p :=
  (mdifferentiableAt_proj E).mdifferentiableWithinAt

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