iUnion_inter_of_antitone — Mathlib

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

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