union_distrib_iInter_left — Mathlib

English

For s: Set α and t(i,j) a family of sets indexed by i and j, the distributive law holds: 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 : Set α) : (t ∪ ⋂ i, s i) = ⋂ i, t ∪ s i :=
  sup_iInf_eq _ _

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