one_lt_inv

Mathlib.Data.ENNReal.Inv

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

English

Let a be an ENNReal. Then 1 < a⁻¹ if and only if a < 1.

Русский

Пусть a — ENNReal. Тогда 1 < a⁻¹ эквивалентно a < 1.

LaTeX

$$$1 < a^{-1} \iff a < 1$$$

Lean4

@[simp]
protected theorem one_lt_inv : 1 < a⁻¹ ↔ a < 1 := by rw [lt_inv_iff_lt_inv, inv_one]

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

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

Разделы

Аффилиация

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