instPosSMulStrictMonoNNReal — Mathlib

English

There is a canonical instance stating that multiplying ENNReal by a positive NNReal is strictly increasing: If a < b then r • a < r • b for r > 0.

Русский

Существует каноническое свойство, что умножение ENNReal на положительное NNReal строго возрастает: если a < b, то r • a < r • b при r > 0.

LaTeX

$$$ \forall a,b \in ENNReal, a < b \Rightarrow (\forall r \in NNReal, r > 0 \Rightarrow r \cdot a < r \cdot b). $$$

Lean4

instance : PosSMulStrictMono ℝ≥0 ℝ≥0∞ where
  smul_lt_smul_of_pos_left _r hr _a _b hab := ENNReal.mul_lt_mul_left' (coe_pos.2 hr).ne' coe_ne_top hab

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