mdifferentiableOn_zeroSection — Mathlib

English

The coordinate change map L between two trivializations is differentiable on their base intersection.

Русский

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

LaTeX

$$$$MDifferentiableOn IB 𝓘(\mathbb{k}, F \to_L[\mathbb{k}] F) (e.coordChangeL 𝕜 e' b) (e.baseSet \cap e'.baseSet).$$$$

Lean4

theorem mdifferentiableOn_zeroSection {t : Set B} : MDifferentiableOn IB (IB.prod 𝓘(𝕜, F)) (zeroSection F E) t :=
  (mdifferentiable_zeroSection _ _).mdifferentiableOn

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