toPosSMulStrictMono — Mathlib

English

If a > 0 and the action is order-preserving on nonnegative elements, then whenever b1 < b2 in β, we have a • b1 < a • b2.

Русский

Если a > 0 и действие сохраняет порядок на неположительных элементах, то при b1 < b2 в β имеет место a • b1 < a • b2.

LaTeX

$$$\\forall a>0,\\; \\forall b_1,b_2 \\in β,\\; b_1 < b_2 \\implies a \\cdot b_1 < a \\cdot b_2$$$

Lean4

theorem toPosSMulStrictMono [PosSMulMono α β] : PosSMulStrictMono α β :=
  ⟨fun _a ha _b₁ _b₂ hb ↦
    (smul_le_smul_of_nonneg_left hb.le ha.le).lt_of_ne <| (smul_right_injective _ ha.ne').ne hb.ne⟩

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