toNNReal_inv

Mathlib.Data.ENNReal.Inv

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

Lean4

@[simp]
theorem toNNReal_inv (a : ℝ≥0∞) : a⁻¹.toNNReal = a.toNNReal⁻¹ := by
  cases a with
  | top => simp
  | coe a =>
    rcases eq_or_ne a 0 with (rfl | ha); · simp
    rw [← coe_inv ha, toNNReal_coe, toNNReal_coe]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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