English
For finite index sets and a family f(i) monotone, the equality iSup j iInf i f(i,j) = iInf i iSup j f(i,j) holds.
Русский
Для конечного множества индексов и монотонного семейства f(i) выполняется равенство.
LaTeX
$$$\text{finite}(\iota) \Rightarrow \big(\forall i, \text{Monotone}(f(i))\big) \Rightarrow \big(\big\vee_j \big(\big\wedge_i f(i,j)\big)\big) = \big(\big\wedge_i \big(\big\vee_j f(i,j)\big)\big).$$$
Lean4
theorem iSup_iInf_of_monotone {ι ι' α : Type*} [Finite ι] [Preorder ι'] [Nonempty ι'] [IsDirected ι' (· ≤ ·)]
[Order.Frame α] {f : ι → ι' → α} (hf : ∀ i, Monotone (f i)) : ⨆ j, ⨅ i, f i j = ⨅ i, ⨆ j, f i j := by
simpa only [iInf_univ] using finite_univ.iSup_biInf_of_monotone fun i _ => hf i
