English
The supremum operation commutes with a two-argument supremum construction: taking sup over b then over c equals taking sup over c then over b with the appropriate function f.
Русский
Операция супремума смешивается как две переменные: верхний предел по b и затем по c равен верхнему пределу по c и затем по b для соответствующей функции f.
LaTeX
$$$\displaystyle (s.sup (\lambda b. t.sup (f\,b))) = t.sup (\lambda c. s.sup (\lambda b. f\,b\,c))$$$
Lean4
protected theorem sup_comm (s : Finset β) (t : Finset γ) (f : β → γ → α) :
(s.sup fun b => t.sup (f b)) = t.sup fun c => s.sup fun b => f b c :=
eq_of_forall_ge_iff fun a => by simpa using forall₂_swap
