le_coe_toReal

Mathlib.Data.EReal.Basic

URI: https://scilib.ai/kg/mathlib#EReal.le_coe_toReal

← MathLib Explorer

English

If x ≠ ⊤, then x ≤ x.toReal.

Русский

Если x ≠ ⊤, то x ≤ x.toReal.

LaTeX

$$$x \neq \top \Rightarrow x \le x^{\mathrm{toReal}}$$$

Lean4

theorem le_coe_toReal {x : EReal} (h : x ≠ ⊤) : x ≤ x.toReal :=
  by
  by_cases h' : x = ⊥
  · simp only [h', bot_le]
  · simp only [le_refl, coe_toReal h h']

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

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

Разделы

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

Аффилиация

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