toReal_le_coe_of_le_coe

Mathlib.Data.ENNReal.Basic

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

← MathLib Explorer

English

If a ≤ ↑b for ENNReal a and NNReal b, then a.toReal ≤ b.

Русский

Если a ≤ ↑b для ENNReal a и NNReal b, тогда a.toReal ≤ b.

LaTeX

$$$ a \le \uparrow b \implies a.toReal \le b $$$

Lean4

theorem toReal_le_coe_of_le_coe {a : ℝ≥0∞} {b : ℝ≥0} (h : a ≤ b) : a.toReal ≤ b :=
  by
  lift a to ℝ≥0 using ne_top_of_le_ne_top coe_ne_top h
  simpa using h

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

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

Разделы

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

Аффилиация

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