isVonNBounded_covers — Mathlib

English

The union of all von Neumann bounded sets is the whole space.

Русский

Объединение всех ограниченных по фон Нейману множеств образует всю пространство.

LaTeX

$$$\\bigcup\\_{X\\;:\\;\\operatorname{IsVonNBounded}_{\\mathbb{k}}} X = \\mathsf{univ}$$$

Lean4

/-- The union of all bounded set is the whole space. -/
theorem isVonNBounded_covers : ⋃₀ setOf (IsVonNBounded 𝕜) = (Set.univ : Set E) :=
  Set.eq_univ_iff_forall.mpr fun x => Set.mem_sUnion.mpr ⟨{ x }, isVonNBounded_singleton _, Set.mem_singleton _⟩

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