isVonNBounded_biUnion — Mathlib

English

Let I be a finite set and for each i ∈ I let s_i ⊆ E be a subset. Then the boundedness of the union ⋃_{i∈I} s_i with respect to 𝕜 is equivalent to the boundedness of every s_i with i ∈ I.

Русский

Пусть I — конечное множество индексов, и для каждого i ∈ I имеется подмножество s_i ⊆ E. Тогда VN‑ограниченность объединения ⋃_{i∈I} s_i равносильна VN‑ограниченности каждого s_i.

LaTeX

$$$IsVonNBounded 𝕜\left(\bigcup_{i\in I} s_i\right) \iff \forall i\in I,\ IsVonNBounded 𝕜(s_i)$$$

Lean4

theorem isVonNBounded_biUnion {ι : Type*} {I : Set ι} (hI : I.Finite) {s : ι → Set E} :
    IsVonNBounded 𝕜 (⋃ i ∈ I, s i) ↔ ∀ i ∈ I, IsVonNBounded 𝕜 (s i) :=
  by
  have _ := hI.to_subtype
  rw [biUnion_eq_iUnion, isVonNBounded_iUnion, Subtype.forall]

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