toNNReal_div

Mathlib.Data.ENNReal.Inv

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

← MathLib Explorer

English

For ENNReal a,b, we have (a/b).toNNReal = a.toNNReal / b.toNNReal.

Русский

Для ENNReal a,b выполняется (a/b).toNNReal = a.toNNReal / b.toNNReal.

LaTeX

$$$ (a/b).toNNReal = a.toNNReal / b.toNNReal $$$

Lean4

@[simp]
theorem toNNReal_div (a b : ℝ≥0∞) : (a / b).toNNReal = a.toNNReal / b.toNNReal := by
  rw [div_eq_mul_inv, toNNReal_mul, toNNReal_inv, div_eq_mul_inv]

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

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

Разделы

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

Аффилиация

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