differentiable_snd

Mathlib.Analysis.Calculus.FDeriv.Prod

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

English

snd is differentiable as a projection.

Русский

snd является проекцией и дифференцируема.

LaTeX

$$differentiable_snd : Differentiable 𝕜 Prod.snd$$

Lean4

@[fun_prop]
theorem differentiable_snd : Differentiable 𝕜 (Prod.snd : E × F → F) := fun _ => differentiableAt_snd

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

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

Разделы

Аффилиация

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