one_lt_mul — Mathlib

English

Let M be a monoid with zero; if 1 ≤ a and 1 < b, or 1 < a and 1 ≤ b, then 1 < a b.

Русский

Пусть M — моноид с нулём; если 1 ≤ a и 1 < b, или 1 < a и 1 ≤ b, то 1 < a b.

LaTeX

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

Lean4

@[bound]
protected theorem one_lt_mul [ZeroLEOneClass M₀] [PosMulMono M₀] [MulPosMono M₀] :
    1 ≤ a ∧ 1 < b ∨ 1 < a ∧ 1 ≤ b → 1 < a * b := by rintro (⟨ha, hb⟩ | ⟨ha, hb⟩);
  exacts [one_lt_mul ha hb, one_lt_mul_of_lt_of_le ha hb]

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