mul_le_of_le_one_left' — Mathlib

English

If α has a left-strict-mono multiplication, then left-cancellative property holds: a·x = a·y implies x = y for all a.

Русский

Если умножение слева строго монотонно, то выполняется левое сокращение: a·x = a·y ⇒ x = y.

LaTeX

$$$\\forall a,x,y:\; a\cdot x = a\cdot y \Rightarrow x = y$$$

Lean4

@[to_additive add_le_of_nonpos_left]
theorem mul_le_of_le_one_left' [MulRightMono α] {a b : α} (h : b ≤ 1) : b * a ≤ a :=
  calc
    b * a ≤ 1 * a := mul_le_mul_right' h a
    _ = a := one_mul a

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