English
If s_i and t_i are antitone families of sets (in a directed index with swap), then the union over i of s_i ∩ t_i equals the intersection of the unions: ⋃_i (s_i ∩ t_i) = (⋃_i s_i) ∩ (⋃_i t_i).
Русский
Если s_i и t_i — антимонотонные семейства множеств, то ⋃_i (s_i ∩ t_i) = (⋃_i s_i) ∩ (⋃_i t_i).
LaTeX
$$$ \bigcup_i (s_i \cap t_i) = (\bigcup_i s_i) \cap (\bigcup_i t_i) $$$
Lean4
theorem iUnion_inter_of_antitone {ι α} [Preorder ι] [IsDirected ι (swap (· ≤ ·))] {s t : ι → Set α} (hs : Antitone s)
(ht : Antitone t) : ⋃ i, s i ∩ t i = (⋃ i, s i) ∩ ⋃ i, t i :=
iSup_inf_of_antitone hs ht