le_inv_iff_le_inv

Mathlib.Data.ENNReal.Inv

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

English

For ENNReal, a ≤ b⁻¹ iff b⁻¹ ≤ a⁻¹.

Русский

Для ENNReal, a ≤ b⁻¹ ⇔ b⁻¹ ≤ a⁻¹.

LaTeX

$$$a \le b^{-1} \iff b^{-1} \le a^{-1}$$$

Lean4

theorem le_inv_iff_le_inv : a ≤ b⁻¹ ↔ b ≤ a⁻¹ := by simpa only [inv_inv] using @ENNReal.inv_le_inv a⁻¹ b

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

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

Разделы

Аффилиация

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