preimage_coe_Iic — Mathlib

English

Real.toEReal^{-1}(Iic(y)) = Iic(y) for any y in ℝ.

Русский

Real.toEReal^{-1}(Iic(y)) = Iic(y) для каждого y ∈ ℝ.

LaTeX

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

Lean4

@[simp]
theorem preimage_coe_Iic (y : ℝ) : Real.toEReal ⁻¹' Iic y = Iic y :=
  by
  change (WithBot.some ∘ WithTop.some) ⁻¹' (Iic (WithBot.some (WithTop.some y))) = _
  refine preimage_comp.trans ?_
  simp only [WithBot.preimage_coe_Iic, WithTop.preimage_coe_Iic]

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