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