neg_of_mul_pos_left

Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic

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

← MathLib Explorer

English

If ab>0 and b≤0, then a<0.

Русский

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

LaTeX

$$$0 < a b \;\Rightarrow\; a<0 \text{ если } b\le 0$$$

Lean4

theorem neg_of_mul_pos_left [PosMulMono α] [MulPosMono α] (h : 0 < a * b) (ha : b ≤ 0) : a < 0 :=
  ((pos_and_pos_or_neg_and_neg_of_mul_pos h).resolve_left fun h => h.2.not_ge ha).1

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

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

Разделы

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

Аффилиация

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