preimage_coe_Iio_top

Mathlib.Data.EReal.Basic

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

← MathLib Explorer

English

Real.toEReal^{-1}(Iio ⊤) equals univ.

Русский

Real.toEReal^{-1}(Iio ⊤) равен univ.

LaTeX

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

Lean4

@[simp]
theorem preimage_coe_Iio_top : Real.toEReal ⁻¹' Iio ⊤ = univ :=
  by
  change (WithBot.some ∘ WithTop.some) ⁻¹' (Iio (WithBot.some ⊤)) = _
  refine preimage_comp.trans ?_
  simp only [WithBot.preimage_coe_Iio, WithTop.preimage_coe_Iio_top]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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