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