image_coe_Ico — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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