English
For finite s and an antitone family f(i), the interchange identity holds with iSup and iInf swapped on the opposite order.
Русский
Для конечного множества и антимонотонной семейств f(i) верна формула обмена iSup и iInf в противоположном порядке.
LaTeX
$$$\text{finite}(s) \Rightarrow (\forall i \in s, \text{Antitone } 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 iSup_biInf_of_antitone {ι ι' α : Type*} [Preorder ι'] [Nonempty ι'] [IsDirected ι' (swap (· ≤ ·))]
[Order.Frame α] {s : Set ι} (hs : s.Finite) {f : ι → ι' → α} (hf : ∀ i ∈ s, Antitone (f i)) :
⨆ j, ⨅ i ∈ s, f i j = ⨅ i ∈ s, ⨆ j, f i j :=
@Finite.iSup_biInf_of_monotone ι ι'ᵒᵈ α _ _ _ _ _ hs _ fun i hi => (hf i hi).dual_left
