toPosSMulStrictMono_rat — Mathlib

English

There is a instance making Rat act by a strictly monotone action on α, and hence providing PosSMulStrictMono on α.

Русский

Существует инстанс, делающий Rat строго монотонным действием на α, давая PosSMulStrictMono на α.

LaTeX

$$$\\text{PosSMulStrictMono}_{\\mathbb{Q}_{\\ge 0}}(\\alpha)$$$

Lean4

instance toPosSMulStrictMono_rat : PosSMulStrictMono ℚ≥0 α where
  smul_lt_smul_of_pos_left q hq a b
    hab := by rw [NNRat.smul_def, NNRat.smul_def]; exact mul_lt_mul_of_pos_left hab <| NNRat.cast_pos.2 hq

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