_example

Mathlib.Geometry.Manifold.IsManifold.Basic

URI: https://scilib.ai/kg/mathlib#IsManifold._example

English

The empty space is a C^n-manifold w.r.t. any charted space and model.

Русский

Пустое множество образует C^n-многообразие относительно любой структуры-charted и любой модели.

LaTeX

$$IsEmpty(M) ⇒ IsManifold(I,n,M)$$

Lean4

example [Unique E] : IsManifold (𝓘(𝕜, E)) n (Fin 2) :=
  of_discreteTopology _

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

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

Разделы

Аффилиация

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