image_coe_Ioc — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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