instBoundedSpaceMultiplicative

Mathlib.Topology.Bornology.Constructions

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

English

If α is a bounded space, then Multiplicative α is bounded.

Русский

Если пространство α ограничено, то и его мультипликативное обобщение (Multiplicative α) ограничено.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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