mul_lt_one_of_nonneg_of_lt_one_right

English

Let M be a monoid with zero equipped with a preorder. If a ≤ 1 and 0 ≤ b < 1, then a b < 1.

Русский

Пусть M — моноид с нулём и заданном порядке. Если a ≤ 1 и 0 ≤ b < 1, то a b < 1.

LaTeX

$$$ (a \le 1) \\land (0 \\le b) \\land (b < 1) \\Rightarrow a b < 1 $$$

Lean4

theorem mul_lt_one_of_nonneg_of_lt_one_right [MulPosMono M₀] (ha : a ≤ 1) (hb₀ : 0 ≤ b) (hb : b < 1) : a * b < 1 :=
  (mul_le_of_le_one_left hb₀ ha).trans_lt hb

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