smul_le_iff_le_one_left

Mathlib.Algebra.Order.Module.Defs

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

← MathLib Explorer

English

For b>0, a•b ≤ b is equivalent to a ≤ 1.

Русский

Для b>0, a•b ≤ b эквивалентно a ≤ 1.

LaTeX

$$$$ b > 0 \Rightarrow (a \cdot b \le b \iff a \le 1) $$$$

Lean4

@[simp]
theorem smul_le_iff_le_one_left [SMulPosMono α β] [SMulPosReflectLE α β] (hb : 0 < b) : a • b ≤ b ↔ a ≤ 1 :=
  Iff.trans (by rw [one_smul]) (smul_le_smul_iff_of_pos_right hb)

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

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

Разделы

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

Аффилиация

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