contMDiffAt_snd

Mathlib.Geometry.Manifold.ContMDiff.Constructions

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

English

The smoothness of the second projection follows from the main ContMDiff theorem.

Русский

Гладкость второй проекции следует из основного теорема о гладкости.

LaTeX

$$ContMDiff snd$$

Lean4

theorem contMDiffAt_snd {p : M × N} : ContMDiffAt (I.prod J) J n Prod.snd p :=
  contMDiffWithinAt_snd

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

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

Разделы

Аффилиация

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