English
In a completely distributive lattice, for any f : ∀ a, κ a → α, the iterated infimum and supremum commute in the variant iInf_iSup_eq': ⨅ a, ⨆ b, f a b = ⨆ g, ⨅ a, f a (g a).
Русский
В полностью распределимой решетке для любого f существует перестановка сумм и инфиминов: ⨅a ⨆b f(a,b) = ⨆g ⨅a f(a, g(a)).
LaTeX
$$$\\displaystyle \\inf_{a} \\sup_{b} f(a,b) = \\sup_{g} \\inf_{a} f(a, g(a))$$$
Lean4
theorem iInf_iSup_eq' (f : ∀ a, κ a → α) :
let _ := minAx.toCompleteLattice
⨅ i, ⨆ j, f i j = ⨆ g : ∀ i, κ i, ⨅ i, f i (g i) :=
by
let _ := minAx.toCompleteLattice
refine le_antisymm ?_ le_iInf_iSup
calc
_ = ⨅ a : range (range <| f ·), ⨆ b : a.1, b.1 := by simp_rw [iInf_subtype, iInf_range, iSup_subtype, iSup_range]
_ = _ := (minAx.iInf_iSup_eq _)
_ ≤ _ :=
iSup_le fun g => by
refine le_trans ?_ <| le_iSup _ fun a => Classical.choose (g ⟨_, a, rfl⟩).2
refine le_iInf fun a => le_trans (iInf_le _ ⟨range (f a), a, rfl⟩) ?_
rw [← Classical.choose_spec (g ⟨_, a, rfl⟩).2]
