mul_finset_sup — Mathlib

English

For any finite set s and NNReal f, multiplying the supremum by r equals the supremum of r times f: r · s.sup f = s.sup (a ↦ r · f a).

Русский

Для конечного множества s и функции f, произведение верхней границы на r равно верхней границе функции a ↦ r·f(a).

LaTeX

$$$\\\\forall {\\\\alpha} (r \\\\in \\\\mathbb{R}_{\\\\ge 0}) (s \\\\in \\\\mathrm{Finset} \\\\alpha) (f : \\alpha \\\\to \\\\mathbb{R}_{\\\\ge 0}), \\\\ r * s.sup f = s.sup (\\\\lambda a. r * f a).$$$

Lean4

theorem mul_finset_sup {α} (r : ℝ≥0) (s : Finset α) (f : α → ℝ≥0) : r * s.sup f = s.sup fun a => r * f a :=
  Finset.comp_sup_eq_sup_comp _ (NNReal.mul_sup r) (mul_zero r)

Похожие утверждения