union_distrib_iInter_right — Mathlib

English

For s(i,j) a two-parameter family and t, the distributive law holds: (⋂_{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

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

Lean4

theorem union_distrib_iInter_right (s : ι → Set α) (t : Set α) : (⋂ i, s i) ∪ t = ⋂ i, s i ∪ t :=
  iInf_sup_eq _ _

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