English
For a finite index set and a collection f(i) monotone in i, the swap of i and j in the iSup and iInf yields equality.
Русский
Для конечного множества индексов и монотонной семейства f(i) взаимно равенство при смене мест i и j в iSup и iInf.
LaTeX
$$$\text{finite}(s) \Rightarrow \text{Monotone}(f(i)) \Rightarrow \big(\big\vee_{j} \big(\big\wedge_{i\in s} f(i,j)\big)\big) = \big(\big\wedge_{i\in s} \big(\big\vee_{j} f(i,j)\big)\big).$$$
Lean4
theorem iInf_biSup_of_monotone {ι ι' α : Type*} [Preorder ι'] [Nonempty ι'] [IsDirected ι' (swap (· ≤ ·))]
[Order.Coframe α] {s : Set ι} (hs : s.Finite) {f : ι → ι' → α} (hf : ∀ i ∈ s, Monotone (f i)) :
⨅ j, ⨆ i ∈ s, f i j = ⨆ i ∈ s, ⨅ j, f i j :=
hs.iSup_biInf_of_antitone (α := αᵒᵈ) fun i hi => (hf i hi).dual_right
