isVonNBounded_iff' — Mathlib

English

In a normed space, von Neumann boundedness is equivalent to boundedness for a nontrivially normed field 𝕜.

Русский

В нормированном пространстве ограниченность по фон Нейману эквивалентна обычной ограниченности для ненулевого поля 𝕜.

LaTeX

$$$\\operatorname{IsVonNBounded}_{\\mathbb{k}}(s) \\iff \\operatorname{IsBounded}(s)$$$

Lean4

theorem isVonNBounded_iff' {s : Set E} : Bornology.IsVonNBounded 𝕜 s ↔ ∃ r : ℝ, ∀ x ∈ s, ‖x‖ ≤ r := by
  rw [NormedSpace.isVonNBounded_iff, isBounded_iff_forall_norm_le]

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