mfderiv_prod_left — Mathlib

English

If f and g are differentiable in the standard sense (MDifferentiable) on their domains, then Prod.map f g is differentiable on the product space with the product model.

Русский

Если f и g дифференциальны в стандартном смысле, тогда Prod.map f g дифференцируемо на произведении.

LaTeX

$$$\forall f,g,\; MDifferentiable I I' f \land MDifferentiable J J' g \Rightarrow MDifferentiable (I.prod J) (I'.prod J') (Prod.map f g)$$$

Lean4

theorem mfderiv_prod_left {x₀ : M} {y₀ : M'} :
    mfderiv I (I.prod I') (fun x => (x, y₀)) x₀ = ContinuousLinearMap.inl 𝕜 (TangentSpace I x₀) (TangentSpace I' y₀) :=
  by
  refine (mdifferentiableAt_id.mfderiv_prod mdifferentiableAt_const).trans ?_
  rw [mfderiv_id, mfderiv_const, ContinuousLinearMap.inl]

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