fst

Mathlib.Geometry.Manifold.ContMDiff.Constructions

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

English

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

Русский

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

LaTeX

$$ContMDiffAt (I.prod J) I n f x → ContMDiffAt J I n (fun x => (f x).1) x$$

Lean4

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

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

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

Разделы

Аффилиация

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