English
Let x and y be nonnegative real numbers. The image of the NNReal interval uIcc(x, y) under the canonical embedding into ENNReal is exactly the ENNReal interval uIcc(x, y). In symbols, (↑) '' uIcc x y = uIcc (x : ℝ≥0∞) y.
Русский
Пусть x и y — неотрицательные числа; образ интервала NNReal [x, y] под стандартным встраиванием в ENNReal равен соответствующему интервалу ENNReal. То есть (↑) '' uIcc x y = uIcc (x : ℝ≥0∞) y.
LaTeX
$$$ (\uparrow) '' \mathrm{uIcc}\ x\ y = \mathrm{uIcc}\ (x : \mathbb{R}_{\ge 0 \infty})\ y $$$
Lean4
@[simp]
theorem image_coe_uIcc (x y : ℝ≥0) : (↑) '' uIcc x y = uIcc (x : ℝ≥0∞) y := by simp [uIcc]