inv_lt_inv

Mathlib.Data.ENNReal.Inv

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

English

For ENNReal, (a/b)⁻¹ = b/a under suitable non-top/non-zero conditions.

Русский

В ENNReal, (a/b)⁻¹ = b/a при подходящих условиях, исключающих ∞ и 0.

LaTeX

$$$\forall a,b \in \mathbb{R}_{\ge 0}^{\infty},\; (b \neq \infty \lor a \neq \infty) \land (b \neq 0 \lor a \neq 0) \Rightarrow (a/b)^{-1} = b/a$$$

Lean4

@[simp]
protected theorem inv_lt_inv : a⁻¹ < b⁻¹ ↔ b < a :=
  inv_strictAnti.lt_iff_gt

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

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

Разделы

Аффилиация

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