smul_le_smul_of_nonneg_left

Mathlib.Algebra.Order.Module.Defs

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

English

If b1 ≤ b2 and a ≥ 0, then a·b1 ≤ a·b2.

Русский

Если b1 ≤ b2 и a ≥ 0, то a·b1 ≤ a·b2.

LaTeX

$$$b_1 \\le b_2 \\Rightarrow a\\ge 0 \\Rightarrow a\\cdot b_1 \\le a\\cdot b_2.$$$

Lean4

@[gcongr]
theorem smul_le_smul_of_nonneg_left [PosSMulMono α β] (hb : b₁ ≤ b₂) (ha : 0 ≤ a) : a • b₁ ≤ a • b₂ :=
  monotone_smul_left_of_nonneg ha hb

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

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

Разделы

Аффилиация

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