of_boundedSpace

Mathlib.Analysis.LocallyConvex.Bounded

URI: https://scilib.ai/kg/mathlib#Bornology.IsVonNBounded.of_boundedSpace

English

If the space is bounded, any set is von Neumann bounded.

Русский

Если пространство ограничено, любое множество VonNBounded.

LaTeX

$$$[BoundedSpace 𝕜] \Rightarrow IsVonNBounded 𝕜 s$$$

Lean4

@[nontriviality]
theorem of_boundedSpace [BoundedSpace 𝕜] {s : Set E} : IsVonNBounded 𝕜 s := fun _ _ ↦ .of_boundedSpace

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

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

Разделы

Аффилиация

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