iUnion₂_inter — Mathlib

English

Distribute union over intersection: (⋃ 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

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

Lean4

theorem iUnion₂_inter (s : ∀ i, κ i → Set α) (t : Set α) : (⋃ (i) (j), s i j) ∩ t = ⋃ (i) (j), s i j ∩ t := by
  simp_rw [iUnion_inter]

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