mul_left_inj_of_comparable — Mathlib

English

If right multiplication is strictly mono and b and c are comparable, then c·a = b·a iff c=b.

Русский

Если правая монотонность и b, c сравнимы, то c·a = b·a тогда и только тогда, когда c=b.

LaTeX

$$$$ \\forall a,b,c \\in \\alpha,\n [MulRightStrictMono \\alpha] \n (b \\le c \\lor c \\le b) \\Rightarrow c \\cdot a = b \\cdot a \\iff c=b $$$$

Lean4

@[to_additive]
theorem mul_left_inj_of_comparable [MulRightStrictMono α] {a b c : α} (h : b ≤ c ∨ c ≤ b) : c * a = b * a ↔ c = b :=
  by
  refine ⟨fun h' => ?_, (· ▸ rfl)⟩
  contrapose h'
  obtain h | h := h
  · exact mul_lt_mul_right' (h.lt_of_ne' h') a |>.ne'
  · exact mul_lt_mul_right' (h.lt_of_ne h') a |>.ne

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