image_coe_uIoo — Mathlib

English

Let x and y be nonnegative real numbers. The image of the NNReal open interval uIoo(x, y) under the canonical embedding into ENNReal is exactly the ENNReal open interval uIoo(x, y). In symbols, (↑) '' uIoo x y = uIoo (x : ℝ≥0∞) y.

Русский

Пусть x и y — неотрицательные числа. Образ открытого интервала NNReal (x, y) под встраиванием в ENNReal равен соответствующему открытому интервалу ENNReal: (↑) '' uIoo x y = uIoo (x : ℝ≥0∞) y.

LaTeX

$$$ (\uparrow) '' \mathrm{uIoo}\ x\ y = \mathrm{uIoo}\ (x : \mathbb{R}_{\ge 0 \infty})\ y $$$

Lean4

@[simp]
theorem image_coe_uIoo (x y : ℝ≥0) : (↑) '' uIoo x y = uIoo (x : ℝ≥0∞) y := by simp [uIoo]

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