English
The von Neumann bornology is the smallest bornology that contains all vonNBounded sets, i.e., a set is bounded iff it is contained in a vonNBounded set.
Русский
Граница фон Неймана задаёт минимальную борологию, включающую все ограниченные по фон Нейману множества; множество ограничено тогда и тогда, когда оно содержится в некотором ограниченном по фон Нейману множестве.
LaTeX
$$$\\text{vonNBornology} = \\operatorname{Bornology\\;ofBounded}\\bigl(\\{ X : \\operatorname{IsVonNBounded}_{\\mathbb{k}}(X)\\} \\bigr) $$$
Lean4
/-- The von Neumann bornology defined by the von Neumann bounded sets.
Note that this is not registered as an instance, in order to avoid diamonds with the
metric bornology. -/
abbrev vonNBornology : Bornology E :=
Bornology.ofBounded (setOf (IsVonNBounded 𝕜)) (isVonNBounded_empty 𝕜 E) (fun _ hs _ ht => hs.subset ht)
(fun _ hs _ => hs.union) isVonNBounded_singleton
