finset_sup_div — Mathlib

English

Division with supremum equals supremum of divisions: s.sup f / r = s.sup (a ↦ f a / r).

Русский

Деление верхней границы на r равно верхней границе делений: s.sup f / r = s.sup (a ↦ f a / r).

LaTeX

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

Lean4

theorem finset_sup_div {α} {f : α → ℝ≥0} {s : Finset α} (r : ℝ≥0) : s.sup f / r = s.sup fun a => f a / r := by
  simp only [div_eq_inv_mul, mul_finset_sup]

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