English
An increasing union distributes over a finite intersection: the union over j of the intersection over i of s(i,j) equals the intersection over i of the union over j of s(i,j).
Русский
Возрастание объединения распределяется по отношению к конечному пересечению: объединение по j и пересечение по i равно пересечению по i и объединению по j.
LaTeX
$$$\bigcup_{j} \big(\bigcap_{i} s(i,j)\big) = \bigcap_{i} \big(\bigcup_{j} s(i,j)\big).$$$
Lean4
/-- An increasing union distributes over finite intersection. -/
theorem iUnion_iInter_of_monotone {ι ι' α : Type*} [Finite ι] [Preorder ι'] [IsDirected ι' (· ≤ ·)] [Nonempty ι']
{s : ι → ι' → Set α} (hs : ∀ i, Monotone (s i)) : ⋃ j : ι', ⋂ i : ι, s i j = ⋂ i : ι, ⋃ j : ι', s i j :=
iSup_iInf_of_monotone hs
