neg_of_mul_neg_left

Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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