le_mul_iff_one_le_left' — Mathlib

English

If a < b then comparing with 1 on the left preserves order: a ≤ 1 ↔ b ≤ 1.

Русский

Если a < b, то слева по отношению к 1 сохраняется неравенство.

LaTeX

$$$ a < b \\rightarrow (a \\le 1 \\Rightarrow b \\le 1)$$$

Lean4

@[to_additive (attr := simp) le_add_iff_nonneg_left]
theorem le_mul_iff_one_le_left' [MulRightMono α] [MulRightReflectLE α] (a : α) {b : α} : a ≤ b * a ↔ 1 ≤ b :=
  Iff.trans (by rw [one_mul]) (mul_le_mul_iff_right a)

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