sup_mul₀ — Mathlib

English

Multiplication on the right distributes over Finset supremum: (sup f)·a = sup (f · a).

Русский

Умножение справа распределяется над верхней гранью по Finset: $(\\sup f)\\cdot a = \\sup (f\\cdot a)$.

LaTeX

$$$\\left(\\sup_{i\\in s} f(i)\\right) \\cdot a = \\sup_{i\\in s} (f(i)\\cdot a)$$$

Lean4

/-- Also see `Finset.sup'_mul₀` for a version for `GroupWithZero`s. -/
theorem sup_mul₀ (s : Finset ι) (f : ι → R) (a : R) : s.sup f * a = s.sup (f · * a) := by
  classical
    induction s using Finset.induction with
  | empty => simp
  | insert _ _ _ IH => simp only [sup_insert, max_mul, ← IH]

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