instMulLeftMono — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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