isVonNBounded_iUnion — Mathlib

English

Let E be a topological space and {s_i} a finite family of subsets of E. Then the union ⋃_i s_i is von Neumann bounded with respect to 𝕜 if and only if each s_i is von Neumann bounded.

Русский

Пусть E — топологическое пространство и {s_i} — конечное семейство подмножеств E. Тогда объединение ⋃_i s_i фон Неймана ограничено по 𝕜 тогда и только тогда, когда каждое s_i ограничено по фон Неймана.

LaTeX

$$$\IsVonNBounded 𝕜\left(\bigcup_i s_i\right) \iff \forall i, \IsVonNBounded 𝕜(s_i)$$$

Lean4

@[simp]
theorem isVonNBounded_iUnion {ι : Sort*} [Finite ι] {s : ι → Set E} :
    IsVonNBounded 𝕜 (⋃ i, s i) ↔ ∀ i, IsVonNBounded 𝕜 (s i) := by
  simp only [IsVonNBounded, absorbs_iUnion, @forall_swap ι]

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