English
For finite index sets, if each f(i) is antitone, then exchanging i and j yields equality: ⨆ j ⨅ i f(i,j) = ⨅ i ⨆ j f(i,j).
Русский
Для конечного множества индексов, если каждое f(i) антимонотонно по i, то выполнение обмена i и j даёт равенство.
LaTeX
$$$\text{finite}(\iota) \Rightarrow \big(\forall i, \text{Antitone}(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 iInf_biSup_of_antitone {ι ι' α : Type*} [Preorder ι'] [Nonempty ι'] [IsDirected ι' (· ≤ ·)] [Order.Coframe α]
{s : Set ι} (hs : s.Finite) {f : ι → ι' → α} (hf : ∀ i ∈ s, Antitone (f i)) :
⨅ j, ⨆ i ∈ s, f i j = ⨆ i ∈ s, ⨅ j, f i j :=
hs.iSup_biInf_of_monotone (α := αᵒᵈ) fun i hi => (hf i hi).dual_right
