preimage_coe_Ioi — Mathlib

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]

Похожие утверждения