English
Let s and t be finite sets and f: β → α with α a semilattice with infimum. Then s.inf (t.inf ∘ f) equals t.inf (s.inf ∘ f). More precisely, s.inf (b ↦ t.inf (f b)) = t.inf (c ↦ s.inf (b ↦ f b c)).
Русский
Пусть s и t — конечные множества, f: β → α, где α — полупорядоченное множество с инфимумом. Тогда инфимум по s от функции b ↦ инфимум по t от (f b) равен инфимуму по t от функции c ↦ инфимум по s от (f b c).
LaTeX
$$$ s.\\inf (\\\\lambda b, t.\\inf (f\\,b)) = t.\\inf (\\\\lambda c, s.\\inf (\\\\lambda b, f\\,b\\,c)) $$$
Lean4
protected theorem inf_comm (s : Finset β) (t : Finset γ) (f : β → γ → α) :
(s.inf fun b => t.inf (f b)) = t.inf fun c => s.inf fun b => f b c :=
@Finset.sup_comm αᵒᵈ _ _ _ _ _ _ _
