snd — Mathlib

English

The map Prod.snd: M × M′ → M′ is MF-differentiable; in particular mdifferentiable (I.prod I') I' Prod.snd.

Русский

Производная MF для Prod.snd существует и равна snd между касательными пространствами.

LaTeX

$$$\mathrm{MDifferentiable}(I\prod I') I' Prod.snd$$$

Lean4

theorem snd {f : N → M × M'} (hf : MDifferentiable J (I.prod I') f) : MDifferentiable J I' fun x => (f x).2 :=
  mdifferentiable_snd.comp hf

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