balanced_iInter₂ — Mathlib

English

If for every i and j the set f(i,j) is balanced, then the intersection over all i and j of f(i,j) is balanced.

Русский

Если для всех i и j множество f(i,j) сбалансировано, то пересечение по всем i и j сбалансировано.

LaTeX

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

Lean4

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

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