smul_lt_smul_of_pos_left

Mathlib.Algebra.Order.Module.Defs

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

← MathLib Explorer

English

If b1 < b2 and a > 0, then a·b1 < a·b2.

Русский

Если b1 < b2 и a > 0, то a·b1 < a·b2.

LaTeX

$$$b_1 < b_2 \\land a > 0 \\Rightarrow a\\cdot b_1 < a\\cdot b_2.$$$

Lean4

@[gcongr]
theorem smul_lt_smul_of_pos_left [PosSMulStrictMono α β] (hb : b₁ < b₂) (ha : 0 < a) : a • b₁ < a • b₂ :=
  strictMono_smul_left_of_pos ha hb

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

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

Разделы

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

Аффилиация

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