div_pos

Mathlib.Data.ENNReal.Inv

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

English

If a ≠ 0 and b ≠ ∞, then a / b > 0 in ENNReal.

Русский

Если a ≠ 0 и b ≠ ∞, то a / b > 0 в ENNReal.

LaTeX

$$$a \neq 0 \land b \neq \infty \Rightarrow 0 < \dfrac{a}{b}$$$

Lean4

protected theorem div_pos (ha : a ≠ 0) (hb : b ≠ ∞) : 0 < a / b :=
  ENNReal.mul_pos ha <| ENNReal.inv_ne_zero.2 hb

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

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

Разделы

Аффилиация

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