fst — Mathlib

English

If f₂ is differentiable, then its first projection is differentiable; the property is propagated via composition with fst.

Русский

Если f₂ дифференцируема, то её первая координата дифференцируема; это свойство сохраняется под композицию с fst.

LaTeX

$$$\text{Differentiable } 𝕜\bigl(\text{Prod.fst} \bigr)\circ f₂$$$

Lean4

@[simp, fun_prop]
protected theorem fst (h : Differentiable 𝕜 f₂) : Differentiable 𝕜 fun x => (f₂ x).1 :=
  differentiable_fst.comp h

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