iUnion_inter_iUnion — Mathlib

English

Let f_i and g_j be 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(\bigcup_i f_i\right) \cap \bigcup_j g_j = \bigcup_i \bigcup_j \bigl( f_i \cap g_j \bigr)$$$

Lean4

theorem iUnion_inter_iUnion {ι κ : Sort*} (f : ι → Set α) (g : κ → Set α) :
    (⋃ i, f i) ∩ ⋃ j, g j = ⋃ i, ⋃ j, f i ∩ g j := by simp_rw [iUnion_inter, inter_iUnion]

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