image_coe_uIcc — Mathlib

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]

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