isVonNBounded_sUnion — Mathlib

English

If S is a finite collection of subsets of E, then the combined union ⋃ S is von Neumann bounded exactly when every member s ∈ S is von Neumann bounded.

Русский

Если S — конечная коллекция подмножеств E, то объединение ⋃S ограничено по фон Нейману тогда и только тогда, когда каждое s ∈ S ограничено по фон Нейману.

LaTeX

$$$IsVonNBounded 𝕜(S.sUnion) \iff ∀ s∈S, IsVonNBounded 𝕜 s$$$

Lean4

theorem isVonNBounded_sUnion {S : Set (Set E)} (hS : S.Finite) : IsVonNBounded 𝕜 (⋃₀ S) ↔ ∀ s ∈ S, IsVonNBounded 𝕜 s :=
  by rw [sUnion_eq_biUnion, isVonNBounded_biUnion hS]

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