balanced_iUnion₂ — Mathlib

English

If a two-parameter family of subsets {f(i,j)} of a vector space E is such that every f(i,j) is balanced, then the union over all i and j is balanced.

Русский

Если для двумерного семейства подмножеств {f(i,j)} пространства E каждый элемент f(i,j) является сбалансированным, то их объединение по всем i и j тоже сбалансировано.

LaTeX

$$$\Big( \forall i, \forall j, \text{Balanced}_{\mathfrak{k}}\big(f(i,j)\big) \Big) \Rightarrow \text{Balanced}_{\mathfrak{k}}\Big( \bigcup_{i} \bigcup_{j} f(i,j) \Big)$$$

Lean4

theorem balanced_iUnion₂ {f : ∀ i, κ i → Set E} (h : ∀ i j, Balanced 𝕜 (f i j)) : Balanced 𝕜 (⋃ (i) (j), f i j) :=
  balanced_iUnion fun _ => balanced_iUnion <| h _

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