snd — Mathlib

English

snd acts as the projection to the second component in the product.

Русский

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

LaTeX

$$fderivWithin_snd {s : Set (E × F)} (hs : UniqueDiffWithinAt 𝕜 s p) : fderivWithin 𝕜 Prod.snd s p = snd 𝕜 E F$$

Lean4

theorem snd (hs : UniqueDiffWithinAt 𝕜 s x) (h : DifferentiableWithinAt 𝕜 f₂ s x) :
    fderivWithin 𝕜 (fun x => (f₂ x).2) s x = (snd 𝕜 F G).comp (fderivWithin 𝕜 f₂ s x) :=
  h.hasFDerivWithinAt.snd.fderivWithin hs

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