image_coe_uIoc — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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