inv_pos

Mathlib.Data.ENNReal.Inv

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

English

In ENNReal, a⁻¹ > 0 if a ≠ ∞.

Русский

В ENNReal, если a ≠ ∞, то a⁻¹ > 0.

LaTeX

$$$a \neq \infty \Rightarrow 0 < a^{-1}$$$

Lean4

@[simp]
protected theorem inv_pos : 0 < a⁻¹ ↔ a ≠ ∞ :=
  pos_iff_ne_zero.trans ENNReal.inv_ne_zero

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

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

Разделы

Аффилиация

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