neg_of_mul_neg_right

Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic

URI: https://scilib.ai/kg/mathlib#Right.neg_of_mul_neg_right

← MathLib Explorer

English

If ab<0 and b≥0 then a<0.

Русский

Если ab<0 и b≥0, то a<0.

LaTeX

$$$ab<0 \wedge b\ge 0 \Rightarrow a<0$$$

Lean4

theorem neg_of_mul_neg_right [MulPosMono α] (h : a * b < 0) (a0 : 0 ≤ a) : b < 0 :=
  lt_of_not_ge fun b0 : b ≥ 0 => (Right.mul_nonneg a0 b0).not_gt h

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

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

Разделы

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

Аффилиация

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