preimage_coe_Ioo_bot_top

Mathlib.Data.EReal.Basic

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

English

Real.toEReal^{-1}(Ioo(⊥, ⊤)) = univ.

Русский

Real.toEReal^{-1}(Ioo(⊥, ⊤)) = бесконечно множество (univ).

LaTeX

$$$\\\\operatorname{Real.toEReal}^{-1}(\\\\mathrm{Ioo}(\\\\bot, \\\\top)) = \\\\mathrm{univ}$$$

Lean4

@[simp]
theorem preimage_coe_Ioo_bot_top : Real.toEReal ⁻¹' Ioo ⊥ ⊤ = univ :=
  by
  rw [← Ioi_inter_Iio]
  simp

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

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

Разделы

Аффилиация

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