English
Let x, y be real numbers. Then the image of the half-open interval Ico(x, y) under the canonical embedding Real.toEReal is the half-open interval Ico in the extended real, with endpoints Real.toEReal(x) and Real.toEReal(y).
Русский
Пусть x, y — вещественные числа. Тогда образ полузакрытого интервала Ico(x, y) при естественном вложении Real.toEReal равен полузакрытому интервалу Ico с контурами Real.toEReal(x) и Real.toEReal(y) в области EReal.
LaTeX
$$$\\\\{ \\\\operatorname{Real.toEReal}(t) \\\\mid t \\\\in [x,y) \\\\} = \\\\mathrm{Ico}(\\\\operatorname{Real.toEReal}(x), \\\\operatorname{Real.toEReal}(y))$$$
Lean4
@[simp]
theorem image_coe_Ico (x y : ℝ) : Real.toEReal '' Ico x y = Ico ↑x ↑y :=
by
refine (image_comp WithBot.some WithTop.some _).trans ?_
rw [WithTop.image_coe_Ico, WithBot.image_coe_Ico]
rfl
