sup'_mul₀ — Mathlib

English

If a > 0, then multiplying the supremum by a on the right distributes: a · sup' f = sup' (i ↦ a · f(i)).

Русский

Если a > 0, то right-multiplication distributes over supremum: a · sup' f = sup' (a · f(i)).

LaTeX

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

Lean4

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

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