iInter_union_of_monotone — Mathlib

English

If s_i and t_i are monotone families of sets (in a directed index with swap), then the intersection over i of s_i ∪ t_i equals the union of the intersections: ⋂_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

$$$ \bigcap_i (s_i \cup t_i) = (\bigcap_i s_i) \cup (\bigcap_i t_i) $$$

Lean4

theorem iInter_union_of_monotone {ι α} [Preorder ι] [IsDirected ι (swap (· ≤ ·))] {s t : ι → Set α} (hs : Monotone s)
    (ht : Monotone t) : ⋂ i, s i ∪ t i = (⋂ i, s i) ∪ ⋂ i, t i :=
  iInf_sup_of_monotone hs ht

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