iInter_iUnion_of_antitone — Mathlib

English

A decreasing intersection distributes over finite union when the family is Antitone.

Русский

Убывающее пересечение распределяется по конечному объединению для антимонотонной семейства.

LaTeX

$$$\text{finite}(\iota) \Rightarrow \bigcap_{j} \big(\bigcup_{i} s(i,j)\big) = \bigcup_{i} \big(\bigcap_{j} s(i,j)\big).$$$

Lean4

/-- A decreasing intersection distributes over finite union. -/
theorem iInter_iUnion_of_antitone {ι ι' α : Type*} [Finite ι] [Preorder ι'] [IsDirected ι' (· ≤ ·)] [Nonempty ι']
    {s : ι → ι' → Set α} (hs : ∀ i, Antitone (s i)) : ⋂ j : ι', ⋃ i : ι, s i j = ⋃ i : ι, ⋂ j : ι', s i j :=
  iInf_iSup_of_antitone hs

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