max_le_mul_of_one_le — Mathlib

English

Let α be a linearly ordered set with Mul α, MulLeftMono α, MulRightMono α and 1 ≤ a, 1 ≤ b. Then max(a, b) ≤ a · b.

Русский

Пусть α упорядочено линейно и есть умножение. Если 1 ≤ a и 1 ≤ b, то max(a,b) ≤ a·b.

LaTeX

$$$ \max(a,b) \le a \cdot b $$$

Lean4

@[to_additive]
theorem max_le_mul_of_one_le [MulLeftMono α] [MulRightMono α] {a b : α} (ha : 1 ≤ a) (hb : 1 ≤ b) : max a b ≤ a * b :=
  max_le_iff.2 ⟨le_mul_of_one_le_right' hb, le_mul_of_one_le_left' ha⟩

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