le_smul_of_one_le_left

Mathlib.Algebra.Order.Module.Defs

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

← MathLib Explorer

English

If b ≥ 0 and a ≤ 1, then b ≤ a•b.

Русский

Если b ≥ 0 и a ≤ 1, то b ≤ a•b.

LaTeX

$$$$ b \ge 0 \land a \le 1 \Rightarrow b \le a\cdot b $$$$

Lean4

theorem le_smul_of_one_le_left [SMulPosMono α β] (hb : 0 ≤ b) (h : 1 ≤ a) : b ≤ a • b := by
  simpa only [one_smul] using smul_le_smul_of_nonneg_right h hb

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

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

Разделы

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

Аффилиация

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