preimage_coe_Ioo

Mathlib.Data.EReal.Basic

URI: https://scilib.ai/kg/mathlib#EReal.preimage_coe_Ioo

English

Real.toEReal^{-1}(Ioo(x,y)) = Ioo(x,y) for all x,y ∈ ℝ.

Русский

Real.toEReal^{-1}(Ioo(x,y)) = Ioo(x,y) для любых x,y ∈ ℝ.

LaTeX

$$$\\\\operatorname{Real.toEReal}^{-1}(\\\\mathrm{Ioo}(x,y)) = \\\\mathrm{Ioo}(x,y)$$$

Lean4

@[simp]
theorem preimage_coe_Ioo (x y : ℝ) : Real.toEReal ⁻¹' Ioo x y = Ioo x y :=
  by
  simp_rw [← Ioi_inter_Iio]
  simp

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru