English
For any real x, Real.toEReal^{-1}(Ioi(x)) = Ioi(x).
Русский
Для любого вещественного x, Real.toEReal^{-1}(Ioi(x)) = Ioi(x).
LaTeX
$$$\\\\operatorname{Real.toEReal}^{-1}(\\\\mathrm{Ioi}(x)) = \\mathrm{Ioi}(x)$$$
Lean4
@[simp]
theorem preimage_coe_Ioi (x : ℝ) : Real.toEReal ⁻¹' Ioi x = Ioi x :=
by
change (WithBot.some ∘ WithTop.some) ⁻¹' (Ioi (WithBot.some (WithTop.some x))) = _
refine preimage_comp.trans ?_
simp only [WithBot.preimage_coe_Ioi, WithTop.preimage_coe_Ioi]