instOfSomeENatTopOfLEInfty

Mathlib.Geometry.Manifold.IsManifold.Basic

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

English

The model space H is a C^n manifold for any model I and any n.

Русский

Модельное пространство H является манifолдом C^n для любой модели I и любого n.

LaTeX

$$$IsManifold I n H$$$

Lean4

instance {a : WithTop ℕ∞} [IsManifold I ∞ M] [h : LEInfty a] : IsManifold I a M :=
  IsManifold.of_le h.out

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

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

Разделы

Аффилиация

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