min_le_mul_of_one_le_left — Mathlib

English

Let α be a linearly ordered set with Mul α and MulRightMono α and 1 ≤ a. Then min(a, b) ≤ a · b for all b ∈ α.

Русский

Пусть α упорядочено линейно и есть умножение справа; если 1 ≤ a, то для любого b: min(a, b) ≤ a·b.

LaTeX

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

Lean4

@[to_additive]
theorem min_le_mul_of_one_le_left [MulRightMono α] {a b : α} (ha : 1 ≤ a) : min a b ≤ a * b :=
  min_le_iff.2 <| Or.inr <| le_mul_of_one_le_left' ha

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