English
Let s be a finite set of indices, t a family of finite sets, and f a function on the sigma-structure. Then the supremum of f over all pairs (i, a) with i ∈ s and a ∈ t(i) equals the supremum over i ∈ s of the supremum over a ∈ t(i) of f(i,a).
Русский
Пусть s — конечное множество индексов, t — семейство конечных множеств, а f — функция над сигма-структурой. Тогда наибольшая величина (верхняя граница) значения f по всем парам (i, a) с i ∈ s и a ∈ t(i) равна наибольшей величине по i ∈ s от наибольших значений f(i,a) по a ∈ t(i).
LaTeX
$$$$ (s.\\sigma t).\\mathrm{sup}\, f = s.\\mathrm{sup}\\,\\bigl( i \\mapsto (t(i)).\\mathrm{sup}\\, (b \\mapsto f\\langle i,b\\rangle) \\bigr) $$$$
Lean4
theorem sup_sigma [SemilatticeSup β] [OrderBot β] : (s.sigma t).sup f = s.sup fun i => (t i).sup fun b => f ⟨i, b⟩ :=
by
simp only [le_antisymm_iff, Finset.sup_le_iff, mem_sigma, and_imp, Sigma.forall]
exact
⟨fun i a hi ha => (le_sup hi).trans' <| le_sup (f := fun a => f ⟨i, a⟩) ha, fun i hi a ha =>
le_sup <| mem_sigma.2 ⟨hi, ha⟩⟩
