contMDiffOn_fst

Mathlib.Geometry.Manifold.ContMDiff.Constructions

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

English

Reiterates that the first projection from a product is C^n.

Русский

Повторение: первая проекция — C^n.

LaTeX

$$ContMDiffWithinAt (I.prod J) I n Prod.fst s p$$

Lean4

theorem contMDiffOn_fst {s : Set (M × N)} : ContMDiffOn (I.prod J) I n Prod.fst s := fun _ _ => contMDiffWithinAt_fst

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

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

Разделы

Аффилиация

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