iUnion_inter_subset — Mathlib

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

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