balanced_iUnion — Mathlib

English

If each f(i) is balanced, then the union over i of f(i) is balanced.

Русский

Если каждое f(i) сбалансировано, то объединение по if(i) сбалансировано.

LaTeX

$$Balanced 𝕜 (\\bigcup_i f_i) where ∀ i, Balanced 𝕜 (f_i)$$

Lean4

theorem balanced_iUnion {f : ι → Set E} (h : ∀ i, Balanced 𝕜 (f i)) : Balanced 𝕜 (⋃ i, f i) := fun _a ha =>
  (smul_set_iUnion _ _).subset.trans <| iUnion_mono fun _ => h _ _ ha

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