instMulRightMono — Mathlib

English

For fixed y, the map x ↦ x * y is order-preserving: if x ≤ z then x * y ≤ z * y.

Русский

Для фиксированного y отображение x ↦ x · y сохраняет порядок: если x ≤ z, то x · y ≤ z · y.

LaTeX

$$$$ x \le z \implies x \cdot y \le z \cdot y \quad \text{for all } y \in \alpha $$$$

Lean4

@[to_additive]
instance : MulRightMono α where
  elim := by
    intro _ _ _; simp only; intro
    rwa [← left_eq_sup, ← sup_mul_distrib, sup_of_le_left]

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