ofReal_toReal_le

Mathlib.Data.ENNReal.Basic

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

English

For any a ∈ ENNReal, the finite part satisfies ofReal(a.toReal) ≤ a.

Русский

Для любого a ∈ ENNReal, ENNReal.ofReal(a.toReal) ≤ a.

LaTeX

$$$\operatorname{ofReal}(a.toReal) \le a$$$

Lean4

theorem ofReal_toReal_le {a : ℝ≥0∞} : ENNReal.ofReal a.toReal ≤ a :=
  if ha : a = ∞ then ha.symm ▸ le_top else le_of_eq (ofReal_toReal ha)

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

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

Разделы

Аффилиация

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