differentiableOn_fst — Mathlib

English

Differentiability of fst is inherited by functions into Prod; the derivative of the first coordinate is the projection.

Русский

Дифференцируемость fst сохраняется при переходе к функции в Prod; производная по первой координате — проекция.

LaTeX

$$$\text{DifferentiableWithinAt } 𝕜\big(\text{Prod.fst}\big) s x$$$

Lean4

@[fun_prop]
theorem differentiableOn_fst {s : Set (E × F)} : DifferentiableOn 𝕜 Prod.fst s :=
  differentiable_fst.differentiableOn

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