iInter_iUnion_of_monotone — Mathlib

English

Same as previous: an increasing intersection distributes over finite union.

Русский

То же, что и ранее: возрастание пересечения распределяется по конечному объединению.

LaTeX

$$$\bigcap_{j} \big(\bigcup_{i} s(i,j)\big) = \bigcup_{i} \big(\bigcap_{j} s(i,j)\big).$$$

Lean4

/-- An increasing intersection distributes over finite union. -/
theorem iInter_iUnion_of_monotone {ι ι' α : Type*} [Finite ι] [Preorder ι'] [IsDirected ι' (swap (· ≤ ·))] [Nonempty ι']
    {s : ι → ι' → Set α} (hs : ∀ i, Monotone (s i)) : ⋂ j : ι', ⋃ i : ι, s i j = ⋃ i : ι, ⋂ j : ι', s i j :=
  iInf_iSup_of_monotone hs

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