image_coe_Icc — Mathlib

English

The image of a closed real interval under Real.toEReal is the corresponding closed interval in EReal.

Русский

Образ закрытого вещественного отрезка под Real.toEReal есть соответствующий закрытый отрезок в EReal.

LaTeX

$$$\mathrm{Real.toEReal}'' \mathrm{Icc}\, x\, y = \mathrm{Icc}\, x^{\mathrm{EReal}} \; y^{\mathrm{EReal}}$$$

Lean4

@[simp]
theorem image_coe_Icc (x y : ℝ) : Real.toEReal '' Icc x y = Icc ↑x ↑y :=
  by
  refine (image_comp WithBot.some WithTop.some _).trans ?_
  rw [WithTop.image_coe_Icc, WithBot.image_coe_Icc]
  rfl

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