coe_toReal_le — Mathlib

English

For x ≠ ⊥, the real-to-EReal embedding of x.toReal is below x: toReal(x) toEReal ≤ x.

Русский

Для x ≠ ⊥, отображение x.toReal в EReal лежит не выше x: (toReal(x))^{toEReal} ≤ x.

LaTeX

$$$(\mathrm{toReal}(x))\mathrm{toEReal} \le x \quad \text{for } x \neq \bot$$

Lean4

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

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