English
For any real x, the image of the ray Ioi(x) under Real.toEReal is the ray Ioo(x.toEReal, ⊤) in EReal.
Русский
Пусть x — вещественное число. Образ луча Ioi(x) при Real.toEReal равен лучу Ioo(x.toEReal, ⊤) в EReal.
LaTeX
$$$\\\\operatorname{Set.image}(\\\\operatorname{Real.toEReal}, \\\\mathrm{Ioi}(x)) = \\\\mathrm{Ioo}(\\\\operatorname{Real.toEReal}(x), \\\\top)$$$
Lean4
@[simp]
theorem image_coe_Ioi (x : ℝ) : Real.toEReal '' Ioi x = Ioo ↑x ⊤ :=
by
refine (image_comp WithBot.some WithTop.some _).trans ?_
rw [WithTop.image_coe_Ioi, WithBot.image_coe_Ioo]
rfl