toNNReal_sub

Mathlib.Data.ENNReal.Operations

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

← MathLib Explorer

English

For ENNReal a,b with b ≠ ∞, (a − b).toNNReal = a.toNNReal − b.toNNReal.

Русский

Для a,b ∈ ENNReal с b ≠ ∞, (a − b).toNNReal = a.toNNReal − b.toNNReal.

LaTeX

$$$ (b \neq \infty) \Rightarrow (a - b)^{\mathrm{toNNReal}} = a^{\mathrm{toNNReal}} - b^{\mathrm{toNNReal}} $$$

Lean4

@[simp]
theorem toNNReal_sub (hb : b ≠ ∞) : (a - b).toNNReal = a.toNNReal - b.toNNReal := by lift b to ℝ≥0 using hb;
  induction a <;> simp [← coe_sub]

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

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

Разделы

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

Аффилиация

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