fst

Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions

URI: https://scilib.ai/kg/mathlib#MDifferentiable.fst

English

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

Русский

Отображение Prod.snd является MF-дифференцируемым.

LaTeX

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

Lean4

theorem fst {f : N → M × M'} (hf : MDifferentiable J (I.prod I') f) : MDifferentiable J I fun x => (f x).1 :=
  mdifferentiable_fst.comp hf

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

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

Разделы

Аффилиация

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