preimage_coe_Iio — Mathlib

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]

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