image_coe_Iio — Mathlib

English

For real x, the image of Iio(x) under Real.toEReal is Ioo(⊥, x.toEReal) in EReal.

Русский

Пусть x — вещественное число. Образ Iio(x) при Real.toEReal равен Ioo(⊥, x.toEReal) в EReal.

LaTeX

$$$\\\\operatorname{Set.image}(\\\\operatorname{Real.toEReal}, \\\\mathrm{Iio}(x)) = \\\\mathrm{Ioo}(\\\\bot, \\\\operatorname{Real.toEReal}(x))$$$

Lean4

@[simp]
theorem image_coe_Iio (x : ℝ) : Real.toEReal '' Iio x = Ioo ⊥ ↑x :=
  by
  refine (image_comp WithBot.some WithTop.some _).trans ?_
  rw [WithTop.image_coe_Iio, WithBot.image_coe_Iio]
  rfl

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