union_distrib_iInter₂_left — Mathlib

English

Let s be a set and t(i,j) a two-parameter family of sets. Then (s ∪ ⋂_{i,j} t(i,j)) = ⋂_{i,j} (s ∪ t(i,j)).

Русский

Пусть s — множество, t(i,j) — семейство множеств. Тогда s ∪ ⋂_{i,j} t(i,j) = ⋂_{i,j} (s ∪ t(i,j)).

LaTeX

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

Lean4

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

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