preimage_coe_Ioc_bot

Mathlib.Data.EReal.Basic

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

English

Real.toEReal^{-1}(Ioc(⊥, y)) = Iic(y).

Русский

Real.toEReal^{-1}(Ioc(⊥, y)) = Iic(y).

LaTeX

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

Lean4

@[simp]
theorem preimage_coe_Ioc_bot (y : ℝ) : Real.toEReal ⁻¹' Ioc ⊥ y = Iic y :=
  by
  rw [← Ioi_inter_Iic]
  simp

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

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

Разделы

Аффилиация

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