mul_pos_iff

Mathlib.Data.ENNReal.Operations

URI: https://scilib.ai/kg/mathlib#ENNReal.mul_pos_iff

English

The product is positive if and only if both factors are positive.

Русский

Произведение положительно тогда, когда оба множителя положительны.

LaTeX

$$$0 < a \cdot b \iff 0 < a \land 0 < b$$$

Lean4

theorem mul_pos_iff : 0 < a * b ↔ 0 < a ∧ 0 < b :=
  CanonicallyOrderedAdd.mul_pos

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

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

Разделы

Аффилиация

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