iInter_union — Mathlib

English

For a family s_i of sets and a fixed set t, the union distributes over the intersection: (⋃_i s_i) ∪ t = ⋂_i (s_i ∪ t).

Русский

Для семейства s_i и фиксированного множества t объединение распределяется по пересечению: (⋃_i s_i) ∪ t = ⋂_i (s_i ∪ t).

LaTeX

$$$ (\bigcup_i s_i) \cup t = \bigcap_i (s_i \cup t) $$$

Lean4

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

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