le_mul_of_le_of_one_le

Mathlib.Algebra.Order.Monoid.Unbundled.Basic

URI: https://scilib.ai/kg/mathlib#le_mul_of_le_of_one_le

← MathLib Explorer

English

If a ≤ 1 and b ≤ 1, then a·b ≤ 1.

Русский

Если a ≤ 1 и b ≤ 1, тогда a·b ≤ 1.

LaTeX

$$$$\forall a,b \in \alpha:\; a \le 1 \land b \le 1 \Rightarrow a\,b \le 1.$$$$

Lean4

@[to_additive]
theorem le_mul_of_le_of_one_le [MulLeftMono α] {a b c : α} (hbc : b ≤ c) (ha : 1 ≤ a) : b ≤ c * a :=
  calc
    b ≤ c := hbc
    _ = c * 1 := (mul_one c).symm
    _ ≤ c * a := mul_le_mul_left' ha c

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru