isBounded_iff_isVonNBounded — Mathlib

English

Restriction of scalars from a nontrivial base field preserves vonNBoundedness.

Русский

Ограничение скаляра с базового поля, не тривиального, сохраняет ограниченность по фон Нейману.

LaTeX

$$$\\operatorname{IsVonNBounded}_{\\mathbb{k}}(s) \\Rightarrow \\operatorname{IsVonNBounded}_{\\mathbb{k}'}(s)$ (при условии соответствующих алгебраических структур и не тривиальности $\\mathbb{k}'$)$$

Lean4

@[simp]
theorem isBounded_iff_isVonNBounded {s : Set E} : @IsBounded _ (vonNBornology 𝕜 E) s ↔ IsVonNBounded 𝕜 s :=
  isBounded_ofBounded_iff _

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