iUnion_inter_of_monotone — Mathlib

English

If s_i and t_i are monotone families of sets (in a directed index), 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_monotone {ι α} [Preorder ι] [IsDirected ι (· ≤ ·)] {s t : ι → Set α} (hs : Monotone s)
    (ht : Monotone t) : ⋃ i, s i ∩ t i = (⋃ i, s i) ∩ ⋃ i, t i :=
  iSup_inf_of_monotone hs ht

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