mdifferentiableAt_proj — Mathlib

English

The projection of a differentiable map into a bundle is differentiable in the base coordinates on the appropriate intersection of base sets.

Русский

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

LaTeX

$$$$MDifferentiableOn IM (IB. prod (modelWithCornersSelf 𝕜 (ContinuousLinearMap (RingHom.id 𝕜) F F)) fun b => \text{coordChangeL}_{b}) (e.baseSet \cap e'.baseSet).$$$$

Lean4

theorem mdifferentiableAt_proj {p : TotalSpace F E} : MDifferentiableAt (IB.prod 𝓘(𝕜, F)) IB (π F E) p :=
  (mdifferentiable_proj E).mdifferentiableAt

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