iInter_union_iInter — Mathlib

English

Let f_i and g_j be families of subsets of α. Then (⋂_i f_i) ∪ (⋂_j g_j) equals ⋂_{i,j} (f_i ∪ g_j).

Русский

Пусть f_i и g_j — семейства подмножеств α. Тогда (⋂_i f_i) ∪ (⋂_j g_j) = ⋂_{i,j} (f_i ∪ g_j).

LaTeX

$$$\left(\bigcap_i f_i\right) \cup \bigcap_j g_j = \bigcap_i \bigcap_j \bigl( f_i \cup g_j \bigr)$$$

Lean4

theorem iInter_union_iInter {ι κ : Sort*} (f : ι → Set α) (g : κ → Set α) :
    (⋂ i, f i) ∪ ⋂ j, g j = ⋂ i, ⋂ j, f i ∪ g j := by simp_rw [iInter_union, union_iInter]

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