preimage_coe_Ioi_bot — Mathlib

English

Real.toEReal^{-1}(Ioi ⊥) equals the entire real line.

Русский

Real.toEReal^{-1}(Ioi ⊥) равен всей множеству вещественных чисел.

LaTeX

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

Lean4

@[simp]
theorem preimage_coe_Ioi_bot : Real.toEReal ⁻¹' Ioi ⊥ = univ :=
  by
  change (WithBot.some ∘ WithTop.some) ⁻¹' (Ioi ⊥) = _
  refine preimage_comp.trans ?_
  simp only [WithBot.preimage_coe_Ioi_bot, preimage_univ]

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