mul_nonpos_iff

Mathlib.Data.EReal.Operations

URI: https://scilib.ai/kg/mathlib#EReal.mul_nonpos_iff

← MathLib Explorer

English

In EReal, if a*b = 0 then a = 0 or b = 0.

Русский

В EReal, если a*b = 0, то либо a = 0, либо b = 0.

LaTeX

$$a * b = 0 \iff a = 0 \lor b = 0$$

Lean4

theorem mul_nonpos_iff {a b : EReal} : a * b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b :=
  by
  nth_rw 1 [← neg_zero]
  rw [EReal.le_neg, ← mul_neg, mul_nonneg_iff, EReal.neg_le, EReal.le_neg, neg_zero]

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

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

Разделы

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

Аффилиация

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