English
Left multiplication by a fixed element is cancellable with respect to the order: a·x ≤ a·y implies x ≤ y.
Русский
Умножение слева на фиксированное значение отменяет порядок: a·x ≤ a·y приводит к x ≤ y.
LaTeX
$$$\forall x,y,\; a\cdot x \le a\cdot y \Rightarrow x \le y$$$
Lean4
/-- An element `a : α` is `MulLECancellable` if `x ↦ a * x` is order-reflecting.
We will make a separate version of many lemmas that require `[MulLeftReflectLE α]` with
`MulLECancellable` assumptions instead. These lemmas can then be instantiated to specific types,
like `ENNReal`, where we can replace the assumption `AddLECancellable x` by `x ≠ ∞`.
-/
@[to_additive /-- An element `a : α` is `AddLECancellable` if `x ↦ a + x` is order-reflecting.
We will make a separate version of many lemmas that require `[MulLeftReflectLE α]` with
`AddLECancellable` assumptions instead. These lemmas can then be instantiated to specific types,
like `ENNReal`, where we can replace the assumption `AddLECancellable x` by `x ≠ ∞`. -/
]
def MulLECancellable [Mul α] [LE α] (a : α) : Prop :=
∀ ⦃b c⦄, a * b ≤ a * c → b ≤ c
