instBoundedSpaceOrderDual

Mathlib.Topology.Bornology.Constructions

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

English

If α is bounded, then its order dual αᵒᵈ is bounded.

Русский

Если пространство α ограничено, то его порядок-два (αᵒᵈ) ограничен.

LaTeX

$$$\\text{BoundedSpace}(\\alpha^\\mathrm{op})$$$

Lean4

instance [BoundedSpace α] : BoundedSpace αᵒᵈ :=
  ‹BoundedSpace α›

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

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

Разделы

Аффилиация

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