modelProdInhabited

Mathlib.Geometry.Manifold.ChartedSpace

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

English

The product of a charted space with itself inherits a canonical self-charted structure.

Русский

Произведение пространства с атласом на себя наследует каноническую самую структуру.

LaTeX

$$chartedSpaceSelf_prod$$

Lean4

instance modelProdInhabited [Inhabited H] [Inhabited H'] : Inhabited (ModelProd H H') :=
  instInhabitedProd

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

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

Разделы

Аффилиация

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