instBoundedSpaceSubtype

Mathlib.Topology.Bornology.Constructions

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

English

If the ambient space is bounded, then any subtype is bounded.

Русский

Если окружающее пространство ограничено, то любой подтип ограничен.

LaTeX

$$$[\\text{BoundedSpace } \\alpha] \\Rightarrow \\text{BoundedSpace}(\\text{Subtype } p)$$$

Lean4

instance [BoundedSpace α] {p : α → Prop} : BoundedSpace (Subtype p) :=
  (IsBounded.all {x | p x}).boundedSpace_subtype

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

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

Разделы

Аффилиация

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