mdifferentiableOn_coordChangeL — Mathlib

English

The total space projection map is MDifferentiable on a set when restricted to that set.

Русский

Проекция полного пространства на множество является MDifferentiable на этом множестве.

LaTeX

$$$$MDifferentiableOn IB (IB.prod 𝓘(\mathbb{k}, F)) IB Bundle.TotalSpace.proj s.$$$$

Lean4

theorem mdifferentiableOn_coordChangeL :
    MDifferentiableOn IB 𝓘(𝕜, F →L[𝕜] F) (fun b : B ↦ (e.coordChangeL 𝕜 e' b : F →L[𝕜] F)) (e.baseSet ∩ e'.baseSet) :=
  (contMDiffOn_coordChangeL e e').mdifferentiableOn le_rfl

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