IsVonNBounded — Mathlib

English

If the ground field 𝕜 is bounded space, then every subset is von Neumann bounded.

Русский

Если 𝕜 является ограниченным пространством, то любой набор E является Von Neumann ограниченным.

LaTeX

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

Lean4

/-- A set `s` is von Neumann bounded if every neighborhood of 0 absorbs `s`. -/
def IsVonNBounded (s : Set E) : Prop :=
  ∀ ⦃V⦄, V ∈ 𝓝 (0 : E) → Absorbs 𝕜 V s

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