finset_sup_mul — Mathlib

English

Supremum distributes over multiplication: s.sup f * r = s.sup (a ↦ f a * r).

Русский

Верхняя граница распределяется по умножению: s.sup f * r = s.sup (a ↦ f a * r).

LaTeX

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

Lean4

theorem finset_sup_mul {α} (s : Finset α) (f : α → ℝ≥0) (r : ℝ≥0) : s.sup f * r = s.sup fun a => f a * r :=
  Finset.comp_sup_eq_sup_comp (· * r) (fun x y => NNReal.sup_mul x y r) (zero_mul r)

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