English
Definition: maps a base-b digit sequence to a real by i ↦ digits(i) · b^{-(i+1)}.
Русский
Определение: отображение последовательности цифр в основание b в действительную величину по правилу i ↦ digits(i) · b^{-(i+1)}.
LaTeX
$$$\{b : \mathbb{N}\} \to (\mathbb{N} \to \mathrm{Fin} b) \to \mathbb{N} \to \mathbb{R}$, $\mathrm{ofDigitsTerm}_{b}(\text{digits})(i) = (\text{digits}(i)) \cdot ((b : \mathbb{R})^{(i+1)})^{-1}$$$
Lean4
/-- Converts a real number `x` from the interval `[0, 1)` into sequence of
its digits in base `b`. -/
noncomputable def digits (x : ℝ) (b : ℕ) [NeZero b] : ℕ → Fin b := fun i ↦ Fin.ofNat _ <| ⌊x * b ^ (i + 1)⌋₊
