toReal_inv

Mathlib.Data.ENNReal.Inv

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

English

For any ENNReal a, (a^{-1}).toReal = (a.toReal)^{-1}.

Русский

Для любого ENNReal a выполняется (a^{-1}).toReal = (a.toReal)^{-1}.

LaTeX

$$$(a^{-1}).toReal = (a.toReal)^{-1}$$$

Lean4

@[simp]
theorem toReal_inv (a : ℝ≥0∞) : a⁻¹.toReal = a.toReal⁻¹ := by simp only [ENNReal.toReal, toNNReal_inv, NNReal.coe_inv]

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

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

Разделы

Аффилиация

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