ennrealRatEmbed — Mathlib

English

The function ennrealRatEmbed maps natural numbers to ENNReal by encoding nonnegative rationals as ENNReal values.

Русский

Функция ennrealRatEmbed отображает натуральное число в ENNReal, кодируя неотрицательные рациональные числа как значения ENNReal.

LaTeX

$$$ ennrealRatEmbed(n) = ENNReal.ofReal\left(\big\lceil\text{decode}(\alpha := \mathbb{Q}, n)\big\rceil\right) $$$

Lean4

/-- A sequence of `ℝ≥0∞`s such that its range is the set of non-negative rational numbers. -/
def ennrealRatEmbed (n : ℕ) : ℝ≥0∞ :=
  ENNReal.ofReal ((Encodable.decode (α := ℚ) n).getD (0 : ℚ))

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