fst

Mathlib.Geometry.Manifold.ContMDiff.Constructions

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

English

The second projection preserves ContMDiffAt: if f is ContMDiffAt, then its second component is ContMDiffAt.

Русский

Вторая компонента сохраняет ContMDiffAt.

LaTeX

$$ContMDiffAt (I.prod J) J n Prod.snd p → ContMDiffAt J I n (fun x => (f x).2) x$$

Lean4

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

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

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

Разделы

Аффилиация

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