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