instBoundedSpaceAdditive

Mathlib.Topology.Bornology.Constructions

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

English

If α is a bounded space, then Additive α is also bounded.

Русский

Если пространство α ограничено, то и его аддитивное обобщение (Additive α) ограничено.

LaTeX

$$$\\text{BoundedSpace}(\\text{Additive } \\alpha)$$$

Lean4

instance [BoundedSpace α] : BoundedSpace (Additive α) :=
  ‹BoundedSpace α›

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

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

Разделы

Аффилиация

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