boundedSpace_val_set_iff

Mathlib.Topology.Bornology.Constructions

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

English

A set s is a bounded space iff s itself is bounded.

Русский

Множество s является ограниченным пространством тогда и только тогда, когда оно ограничено.

LaTeX

$$$\\text{BoundedSpace}(s) \\iff \\operatorname{IsBounded}(s)$$$

Lean4

theorem boundedSpace_val_set_iff {s : Set α} : BoundedSpace s ↔ IsBounded s :=
  boundedSpace_subtype_iff

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

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

Разделы

Аффилиация

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