instPosSMulMono — Mathlib

English

If the scalar is nonnegative and the target family is ordered, then scalar multiplication is monotone in the argument.

Русский

Если скаляр неотрицателен и целевая семейство упорядочено, то умножение на скаляр монотонно по аргументу.

LaTeX

$$$$ \lambda \ge 0,\ f \le g \Rightarrow \lambda \cdot f \le \lambda \cdot g. $$$$

Lean4

instance instPosSMulMono [∀ i, PosSMulMono α (β i)] : PosSMulMono α (Π₀ i, β i) :=
  PosSMulMono.lift _ coe_le_coe coe_smul

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