lt_of_mul_lt_of_one_le_right — Mathlib

English

In a preordered monoid with unit, if a is at least 1 and a·b < c, then b < c.

Русский

В предмордном моноиде с единицей, если a ≥ 1 и a·b < c, то b < c.

LaTeX

$$$\\\\forall a,b,c \\\\\\in \\\\alpha, (a \\\\cdot b < c) \\\\land (1 \\\\le a) \\\\Rightarrow b < c$$$

Lean4

@[to_additive]
theorem lt_of_mul_lt_of_one_le_right [MulRightMono α] {a b c : α} (h : a * b < c) (hle : 1 ≤ a) : b < c :=
  (le_mul_of_one_le_left' hle).trans_lt h

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