image_coe_Ioo — Mathlib

English

For x,y ∈ ℝ≥0, image ENNReal.ofNNReal on Ioo x y equals Ioo ENNReal.ofNNReal x ENNReal.ofNNReal y.

Русский

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

LaTeX

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

Lean4

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

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