English
For i indexing, the union of intersections is contained in the intersection of unions: ⋃_i (s_i ∩ t_i) ⊆ (⋃_i s_i) ∩ (⋃_i t_i).
Русский
Объединение попарных пересечений вложено в пересечение объединений: ⋃_i (s_i ∩ t_i) ⊆ (⋃_i s_i) ∩ (⋃_i t_i).
LaTeX
$$$ \bigcup_i (s_i \cap t_i) \subseteq (\bigcup_i s_i) \cap (\bigcup_i t_i) $$$
Lean4
theorem iUnion_inter_subset {ι α} {s t : ι → Set α} : ⋃ i, s i ∩ t i ⊆ (⋃ i, s i) ∩ ⋃ i, t i :=
le_iSup_inf_iSup s t