snd

Mathlib.Geometry.Manifold.ContMDiff.Constructions

URI: https://scilib.ai/kg/mathlib#ContMDiffAt.snd

English

Projection to the second coordinate from a product is ContMDiffAt.

Русский

Проекция на вторую координату из произведения является ContMDiffAt.

LaTeX

$$$ ContMDiffAt J (I.prod I') n f x \Rightarrow ContMDiffAt J I' n (fun x => (f x).2) x$$

Lean4

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

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

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

Разделы

Аффилиация

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