English
In a completely distributive lattice, for any f : ∀ a, κ a → α, the infimum and supremum commute: ⨅ a, ⨆ b, f a b = ⨆ g, ⨅ a, f a (g a).
Русский
В полностью распределимой решетке справедливо: ⨅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 iSup_iInf_eq (f : ∀ i, κ i → α) :
let _ := minAx.toCompleteLattice
⨆ i, ⨅ j, f i j = ⨅ g : ∀ i, κ i, ⨆ i, f i (g i) :=
by
let _ := minAx.toCompleteLattice
refine le_antisymm iSup_iInf_le ?_
rw [minAx.iInf_iSup_eq']
refine iSup_le fun g => ?_
have ⟨a, ha⟩ : ∃ a, ∀ b, ∃ f, ∃ h : a = g f, h ▸ b = f (g f) :=
of_not_not fun h => by
push_neg at h
choose h hh using h
have := hh _ h rfl
contradiction
refine le_trans ?_ (le_iSup _ a)
refine le_iInf fun b => ?_
obtain ⟨h, rfl, rfl⟩ := ha b
exact iInf_le _ _
