iInter_union_of_antitone — Mathlib

English

If s_i and t_i are antitone families (directed by 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_antitone {ι α} [Preorder ι] [IsDirected ι (· ≤ ·)] {s t : ι → Set α} (hs : Antitone s)
    (ht : Antitone t) : ⋂ i, s i ∪ t i = (⋂ i, s i) ∪ ⋂ i, t i :=
  iInf_sup_of_antitone hs ht

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