mul_lt_iff_lt_one_right' — Mathlib

English

If a·b < b, then a < 1, under right-strict-monotone multiplication and right-reflect LT.

Русский

Если a·b < b, то a < 1 при условии правого строгого монотонного умножения и правого отражения LT.

LaTeX

$$$$\forall a,b \in \alpha:\; a\,b < b \Rightarrow a < 1.$$$$

Lean4

@[to_additive (attr := simp) add_lt_iff_neg_right]
theorem mul_lt_iff_lt_one_right' [MulRightStrictMono α] [MulRightReflectLT α] {a : α} (b : α) : a * b < b ↔ a < 1 :=
  Iff.trans (by rw [one_mul]) (mul_lt_mul_iff_right b)

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