mul_iSup — Mathlib

English

Let a ≥ 0 and f : ι → ℝ≥0. Then a · sup_i f(i) = sup_i (a · f(i)).

Русский

Пусть a ≥ 0 и f : ι → ℝ≥0. Тогда a · sup_i f(i) = sup_i (a · f(i)).

LaTeX

$$$ a \\cdot \\sup_{i \\in \\iota} f(i) = \\sup_{i \\in \\iota} (a \\cdot f(i)) $$$

Lean4

theorem mul_iSup (f : ι → ℝ≥0) (a : ℝ≥0) : (a * ⨆ i, f i) = ⨆ i, a * f i :=
  by
  rw [← coe_inj, NNReal.coe_mul, NNReal.coe_iSup, NNReal.coe_iSup]
  exact Real.mul_iSup_of_nonneg (NNReal.coe_nonneg _) _

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