mdifferentiable_proj — Mathlib

English

A set version: if hψ, hv, hw are differentiable on s, then ψ m (v m) (w m) is differentiable on s.

Русский

На множестве если hψ, hv, hw дифференцируемы на s, то ψ m (v m) (w m) дифференцируемо на s.

LaTeX

$$$$\text{MDifferentiableOn 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)))} s.$$$$

Lean4

theorem mdifferentiable_proj : MDifferentiable (IB.prod 𝓘(𝕜, F)) IB (π F E) := fun x ↦
  by
  have : MDifferentiableAt (IB.prod 𝓘(𝕜, F)) (IB.prod 𝓘(𝕜, F)) id x := mdifferentiableAt_id
  rw [mdifferentiableAt_totalSpace] at this
  exact this.1

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