English
For a finite set s of indices and a family f(i) monotone in i, the iterated supremum and infimum commute: ⨆ j ⨅ i∈s f(i,j) = ⨅ i∈s ⨆ j f(i,j).
Русский
Для конечного множества индексов и семейства f(i) монотонного по i взаимно обращаются верхний и нижний пределы: ⨆ j ⨅ i∈s f(i,j) = ⨅ i∈s ⨆ j f(i,j).
LaTeX
$$$s\text{ finite} \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_monotone {ι ι' α : Type*} [Preorder ι'] [Nonempty ι'] [IsDirected ι' (· ≤ ·)] [Order.Frame α]
{s : Set ι} (hs : s.Finite) {f : ι → ι' → α} (hf : ∀ i ∈ s, Monotone (f i)) :
⨆ j, ⨅ i ∈ s, f i j = ⨅ i ∈ s, ⨆ j, f i j := by
induction s, hs using Set.Finite.induction_on with
| empty => simp [iSup_const]
| insert _ _ ihs =>
rw [forall_mem_insert] at hf
simp only [iInf_insert, ← ihs hf.2]
exact iSup_inf_of_monotone hf.1 fun j₁ j₂ hj => iInf₂_mono fun i hi => hf.2 i hi hj
