fst — Mathlib

English

Within a set s, the MF-derivative of Prod.fst is the fst-operator between the tangent spaces, precisely mfderivWithin (I.prod I') I Prod.fst s x = ContinuousLinearMap.fst 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2).

Русский

Внутри множества s производная MF от Prod.fst равна fst-оператору между касательными пространствами.

LaTeX

$$$mfderivWithin (I\prod I')\, I\, Prod.fst\, s\, x = \mathrm{ContinuousLinearMap.fst}\ 𝕜\; (\mathrm{TangentSpace}\; I\, x.1)\; (\mathrm{TangentSpace}\; I'\, x.2)$$$

Lean4

theorem fst {f : N → M × M'} {x : N} (hf : MDifferentiableAt J (I.prod I') f x) :
    MDifferentiableAt J I (fun x => (f x).1) x :=
  mdifferentiableAt_fst.comp x hf

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