snd — Mathlib

English

The derivative of the snd projection is its projection map, in the strict sense.

Русский

Проекция snd имеет строгую производную, равную самой проекции.

LaTeX

$$HasStrictFDerivAt snd (ContinuousLinearMap.snd 𝕜 E F) p$$

Lean4

@[fun_prop]
protected theorem snd (h : DifferentiableWithinAt 𝕜 f₂ s x) : DifferentiableWithinAt 𝕜 (fun x => (f₂ x).2) s x :=
  differentiableAt_snd.comp_differentiableWithinAt x h

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