preimage_coe_Ioc

Mathlib.Data.EReal.Basic

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

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem preimage_coe_Ioc (x y : ℝ) : Real.toEReal ⁻¹' Ioc x y = Ioc x y :=
  by
  simp_rw [← Ioi_inter_Iic]
  simp

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

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

Разделы

Аффилиация

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