mdifferentiableAt_fst

Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions

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

English

Further instance: the fst projection remains differentiable in the product setting.

Русский

Повторный случай: проекция fst продолжает быть дифференцируемой в произведении.

LaTeX

$$$ mdifferentiableAt_fst {x} : MDifferentiableAt (I.prod I') I Prod.fst x $$$

Lean4

theorem mdifferentiableAt_fst {x : M × M'} : MDifferentiableAt (I.prod I') I Prod.fst x :=
  (hasMFDerivAt_fst x).mdifferentiableAt

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

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

Разделы

Аффилиация

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