English
A double infinitum with two finite sets is symmetric: the nested infima commute up to a renaming of variables, i.e., the expression with s then t equals the expression with t then s.
Русский
Двойной инфимум с двумя конечными множествами симметричен: внутренняя инфимумация по s и t равна инфимумации по t и s при соответствующем отображении.
LaTeX
$$$(s.inf' hs \\; (\\lambda b. t.inf' ht (f\\, b))) = (t.inf' ht (\\lambda c. s.inf' hs (\\lambda b. f b c)))$$$
Lean4
protected theorem inf'_comm {t : Finset γ} (hs : s.Nonempty) (ht : t.Nonempty) (f : β → γ → α) :
(s.inf' hs fun b => t.inf' ht (f b)) = t.inf' ht fun c => s.inf' hs fun b => f b c :=
@Finset.sup'_comm αᵒᵈ _ _ _ _ _ hs ht _
