toReal_sub_of_le

Mathlib.Data.ENNReal.Operations

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

← MathLib Explorer

English

If b ≤ a and a ≠ ∞, then (a − b).toReal = a.toReal − b.toReal.

Русский

Если b ≤ a и a ≠ ∞, то (a − b).toReal = a.toReal − b.toReal.

LaTeX

$$$ (hba : b \le a) (ha : a \neq \infty) \Rightarrow (a - b).toReal = a.toReal - b.toReal $$$

Lean4

@[simp]
theorem toReal_sub_of_le (hba : b ≤ a) (ha : a ≠ ∞) : (a - b).toReal = a.toReal - b.toReal := by
  simp [ENNReal.toReal, ne_top_of_le_ne_top ha hba, toNNReal_mono ha hba]

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

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

Разделы

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

Аффилиация

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