isVonNBounded_empty

Mathlib.Analysis.LocallyConvex.Bounded

URI: https://scilib.ai/kg/mathlib#Bornology.isVonNBounded_empty

English

The empty set is von Neumann bounded.

Русский

Пустое множество Von Neumann ограничено.

LaTeX

$$$ IsVonNBounded 𝕜 ∅$$$

Lean4

@[simp]
theorem isVonNBounded_empty : IsVonNBounded 𝕜 (∅ : Set E) := fun _ _ => Absorbs.empty

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

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

Разделы

Аффилиация

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