English
For nonempty Finsets s of indices, and finite M, the sum of suprema distributes over product indexing: s.sup f + t.sup g = (s × t).sup (i,j ↦ f(i) + g(j)).
Русский
Для непустых множеств индексов s и t выполняется: сумма верхних пределов разнесена по произведению индексов: sup s f + sup t g = sup_{(i,j)∈s×t} (f(i) + g(j)).
LaTeX
$$$s.Nonempty \\to t.Nonempty \\to \\forall f,g: (ι \\to M), (κ \\to M),\\ s.sup f + t.sup g = (s \\times{\\!} \\ t).sup (\\lambda ij, f(i) + g(j)).$$$
Lean4
protected theorem add_sup (hs : s.Nonempty) (f : ι → M) (a : M) : a + s.sup f = s.sup fun i ↦ a + f i := by
rw [← Finset.sup'_eq_sup hs, ← Finset.sup'_eq_sup hs, add_sup'']
