contMDiff_snd

Mathlib.Geometry.Manifold.ContMDiff.Constructions

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

English

The fst projection remains ContMDiff on the inner level for ContMDiff.

Русский

fst гладко на внутреннем уровне.

LaTeX

$$contMDiffWithinAt_fst {s : Set (M × N)} {p : M × N} : ContMDiffWithinAt (I.prod J) I n Prod.fst s p$$

Lean4

theorem contMDiff_snd : ContMDiff (I.prod J) J n (@Prod.snd M N) := fun _ => contMDiffAt_snd

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

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

Разделы

Аффилиация

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