nnrat_of_rat — Mathlib

English

If α is a preorder with a rational action, then the nonnegative rationals act monotonically on α.

Русский

При наличии предорядка на α и рационального действия, ℚ≥0 действует монотонно на α.

LaTeX

$$$q\\in \\mathbb{Q}_{\\ge 0}, a,b\\in \\alpha,\\ a\\le b\\ \\Rightarrow\\ qa\\le qb$$$

Lean4

instance nnrat_of_rat [Preorder α] [MulAction ℚ α] [PosSMulMono ℚ α] : PosSMulMono ℚ≥0 α where
  smul_le_smul_of_nonneg_left _q hq _a₁ _a₂ ha := smul_le_smul_of_nonneg_left (α := ℚ) ha hq

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