English
Real.toEReal^{-1}(Iio(y)) = Iio(y) for any y ∈ ℝ.
Русский
Real.toEReal^{-1}(Iio(y)) = Iio(y) для каждого y ∈ ℝ.
LaTeX
$$$\\\\operatorname{Real.toEReal}^{-1}(\\\\mathrm{Iio}(y)) = \\\\mathrm{Iio}(y)$$$
Lean4
@[simp]
theorem preimage_coe_Iio (y : ℝ) : Real.toEReal ⁻¹' Iio y = Iio y :=
by
change (WithBot.some ∘ WithTop.some) ⁻¹' (Iio (WithBot.some (WithTop.some y))) = _
refine preimage_comp.trans ?_
simp only [WithBot.preimage_coe_Iio, WithTop.preimage_coe_Iio]