English
For real x, y, the image of the half-open interval Ioc(x, y) under Real.toEReal is the corresponding Ioc interval in EReal with endpoints x.toEReal and y.toEReal.
Русский
Пусть x, y — вещественные числа. Образ полузакрытого интервала Ioc(x, y) при Real.toEReal равен соответствующему интервалу Ioc в EReal с границами x.toEReal и y.toEReal.
LaTeX
$$$\\\\operatorname{Set.image}(\\\\operatorname{Real.toEReal}, \\\\mathrm{Ioc}(x,y)) = \\\\mathrm{Ioc}(\\\\operatorname{Real.toEReal}(x), \\\\operatorname{Real.toEReal}(y))$$$
Lean4
@[simp]
theorem image_coe_Ioc (x y : ℝ) : Real.toEReal '' Ioc x y = Ioc ↑x ↑y :=
by
refine (image_comp WithBot.some WithTop.some _).trans ?_
rw [WithTop.image_coe_Ioc, WithBot.image_coe_Ioc]
rfl
