union_distrib_iInter₂_right — Mathlib

English

For s: Set α and t: Set α, the identity (⋂_i (⋂_j t(i,j))) ∪ t = ⋂_i (⋂_j (t(i,j) ∪ t)) holds, reflecting union distribution over a two-dimensional intersection.

Русский

Для двуразмерной пересечения выполняется дистрибутивность объединения над ним: (⋂_{i,j} t(i,j)) ∪ t = ⋂_{i,j} (t(i,j) ∪ t).

LaTeX

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

Lean4

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

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