toSMulPosMono — Mathlib

English

Positivity-preserving property transfers to scalar action; the smul action respects order in β when α acts positively.

Русский

Свойство сохранения знака переносится на скалярное действие; действие умножения уважает порядок в β при положительном основании α.

LaTeX

$$SMulPosMono α β$$

Lean4

instance toSMulPosMono : SMulPosMono α β where
  smul_le_smul_of_nonneg_right _b hb a₁ a₂
    ha := by rw [← sub_nonneg, ← sub_smul]; exact smul_nonneg (sub_nonneg.2 ha) hb

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