instIsManifoldSubtypeMem

Mathlib.Geometry.Manifold.IsManifold.Basic

URI: https://scilib.ai/kg/mathlib#TopologicalSpace.Opens.instIsManifoldSubtypeMem

English

If s is an open subset of M, then the subtype s is a manifold under the induced charted structure.

Русский

Если s — открытое подмножество M, то подсистема s образует множество с индуцированной структурой диаграмм.

LaTeX

$$IsManifold I n s$$

Lean4

instance : IsManifold I n s :=
  { s.instHasGroupoid (contDiffGroupoid n I) with }

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

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

Разделы

Аффилиация

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