image_coe_Icc — Mathlib

English

For x,y ∈ ℝ≥0, (ENNRReal.ofNNReal) on Icc x y equals Icc of ENNReal.ofNNReal x and y.

Русский

Для x,y ∈ ℝ≥0: образ ENNReal.ofNNReal на Icc x y равен Icc (ENNReal.ofNNReal x) (ENNReal.ofNNReal y).

LaTeX

$$$ x,y : \mathbb{R}_{\ge 0} \Rightarrow \operatorname{image} ENNReal.ofNNReal (\mathrm{Icc}\; x\; y) = \mathrm{Icc} (\operatorname{ENNReal.ofNNReal} x) (\operatorname{ENNReal.ofNNReal} y) $$$

Lean4

@[simp]
theorem image_coe_Icc (x y : ℝ≥0) : (↑) '' Icc x y = Icc (x : ℝ≥0∞) y :=
  WithTop.image_coe_Icc

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