range_coe — Mathlib

English

The image of the real-to-EReal embedding consists exactly of all EReal elements except the bottom and the top.

Русский

Образ отображения вещественных чисел в EReal состоит из всех элементов EReal кроме нижнего и верхнего.

LaTeX

$$$\operatorname{range}(\mathrm{Real.toEReal}) = \mathsf{EReal} \setminus \{\bot, \top\}$$$

Lean4

theorem range_coe : range Real.toEReal = {⊥, ⊤}ᶜ := by
  ext x
  induction x <;> simp

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