mul₀_sup' — Mathlib

English

If a > 0, left-multiplication distributes over supremum: a · sup' f = sup' (a · f(i)).

Русский

Если a > 0, левое умножение распределяется над supremum: a · sup' f = sup' (a · f(i)).

LaTeX

$$$a>0 \Rightarrow \Big(\sup'_{i\in s} f(i)\Big) \cdot a = \sup'_{i\in s} (f(i) \cdot a).$$$

Lean4

theorem mul₀_sup' [PosMulReflectLT G₀] (ha : 0 < a) (f : ι → G₀) (s : Finset ι) (hs) :
    a * s.sup' hs f = s.sup' hs fun i ↦ a * f i :=
  map_finset_sup' (OrderIso.mulLeft₀ _ ha) hs f

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