mdifferentiableOn_proj — Mathlib

English

Let hψ, hv, hw be differentiable in the relevant sense; then the map m ↦ ψ(m)(v(m), w(m)) is differentiable at x.

Русский

Пусть hψ, hv, hw дифференцируемы; тогда m ↦ ψ(m)(v(m), w(m)) дифференцируемо в точке x.

LaTeX

$$$$\text{MDifferentiableAt IM (IB. prod 𝓘(\mathbb{k}, F_1 \to_L F_2 \to_L F_3)) n (m \mapsto \mathrm{TotalSpace.mk}' F_3 (b(m)) (\psi m (v m) (w m)))} x.$$$$

Lean4

theorem mdifferentiableOn_proj {s : Set (TotalSpace F E)} : MDifferentiableOn (IB.prod 𝓘(𝕜, F)) IB (π F E) s :=
  (mdifferentiable_proj E).mdifferentiableOn

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