mul_sup₀ — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem mul_sup₀ (s : Finset ι) (f : ι → R) (a : R) : a * s.sup f = s.sup (a * f ·) := by
  classical
    induction s using Finset.induction with
  | empty => simp
  | insert _ _ _ IH => simp only [sup_insert, mul_max, ← IH]

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