inter_iUnion₂ — Mathlib

English

The intersection with a double union distributes over the union: s ∩ ⨆ i j t(i,j) = ⨆ i j (s ∩ t(i,j)).

Русский

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

LaTeX

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

Lean4

theorem inter_iUnion₂ (s : Set α) (t : ∀ i, κ i → Set α) : (s ∩ ⋃ (i) (j), t i j) = ⋃ (i) (j), s ∩ t i j := by
  simp only [inter_iUnion]

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