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