union_iInter₂ — Mathlib

English

The intersection distributes over a double union: (⋂ i (j), s i j) ∪ t = ⋂ i (j), s i j ∪ t.

Русский

Пересечение распределяется по двойному объединению: (⋂ i j s i j) ∪ t = ⋂ i j (s i j ∪ t).

LaTeX

$$$\\\\bigcap_{i} \\\\bigcap_{j} s(i,j) \\\\cup t = \\\\bigcap_{i} \\\\bigcap_{j} (s(i,j) \\\\cup t)$$$

Lean4

theorem union_iInter₂ (s : Set α) (t : ∀ i, κ i → Set α) : (s ∪ ⋂ (i) (j), t i j) = ⋂ (i) (j), s ∪ t i j := by
  simp_rw [union_iInter]

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