lt_of_smul_lt_smul_of_nonpos

Mathlib.Algebra.Order.Module.Defs

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

← MathLib Explorer

English

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

Русский

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

LaTeX

$$$a<0,\ b_1

Lean4

theorem lt_of_smul_lt_smul_of_nonpos [PosSMulReflectLT α β] (h : a • b₁ < a • b₂) (ha : a ≤ 0) : b₂ < b₁ :=
  by
  rw [← neg_neg a, neg_smul, neg_smul (-a), neg_lt_neg_iff] at h
  exact lt_of_smul_lt_smul_of_nonneg_left h (neg_nonneg_of_nonpos ha)

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

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

Разделы

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

Аффилиация

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