div_nonpos_of_nonpos_of_nonneg

Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic

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

← MathLib Explorer

English

If a ≤ 0 and b ≥ 0 in a group with zero, then a / b ≤ 0.

Русский

Если в группе с нулём a ≤ 0 и b ≥ 0, то a / b ≤ 0.

LaTeX

$$$a \le 0 \land b \ge 0 \implies \dfrac{a}{b} \le 0$$$

Lean4

theorem div_nonpos_of_nonpos_of_nonneg (ha : a ≤ 0) (hb : 0 ≤ b) : a / b ≤ 0 := by rw [div_eq_mul_inv];
  exact mul_nonpos_of_nonpos_of_nonneg ha (Right.inv_nonneg.2 hb)

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

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

Разделы

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

Аффилиация

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