English
Let M be an AddCommMonoid with LinearOrder, CanonicallyOrderedAdd, Sub, AddLeftReflectLE, OrderedSub. Then for any s: Finset ι, t: Finset κ, we have sup over s of f plus sup over t of g equals sup over the product s×t of the sum: s.sup f + t.sup g = (s × t).sup (f ∘ proj1 + g ∘ proj2).
Русский
Пусть M — канонически упорядоченный аддитивный коммодиум с линейным порядком, Sub и прочими свойствами. Тогда сумма верхних пределов по f и по g равна верхнему пределу по попарному сложению: s.sup f + t.sup g = (s × t).sup (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
theorem sup_add_sup (hs : s.Nonempty) (ht : t.Nonempty) (f : ι → M) (g : κ → M) :
s.sup f + t.sup g = (s ×ˢ t).sup fun ij ↦ f ij.1 + g ij.2 := by
simp only [Finset.sup_add hs, Finset.add_sup ht, Finset.sup_product_left]
