range_coe' — Mathlib

English

The image of NNReal in ENNReal equals the finite ENNReal numbers, i.e., the set { x ∈ ENNReal : x < ∞ }.

Русский

Образ вложения NNReal в ENNReal совпадает с множеством конечных элементов ENNReal, то есть { x ∈ ENNReal : x < ∞ }.

LaTeX

$$$\mathrm{range}(\mathrm{ofNNReal}) = \{ x \in \mathbb{R}_{\ge 0}^{\infty} : x < \infty \} $$$

Lean4

theorem range_coe' : range ofNNReal = Iio ∞ :=
  WithTop.range_coe

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