differentiableOn_snd

Mathlib.Analysis.Calculus.FDeriv.Prod

URI: https://scilib.ai/kg/mathlib#differentiableOn_snd

English

The derivative of snd equals the second projection map.

Русский

Производная snd равна второй проекции.

LaTeX

$$fderiv_snd : fderiv 𝕜 Prod.snd p = snd 𝕜 E F$$

Lean4

@[fun_prop]
theorem differentiableOn_snd {s : Set (E × F)} : DifferentiableOn 𝕜 Prod.snd s :=
  differentiable_snd.differentiableOn

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru