English
If 0 < e and n < 10^e, then the decimal representation length of n is at most e.
Русский
Если 0 < e и n < 10^e, тогда десятичное представление n имеет длину не более e.
LaTeX
$$$\\forall n,e \\in \\mathbb{N},\\ 0 < e \\land n < 10^{e} \\Rightarrow (\\mathrm{Nat.repr}\\,n).length \\le e$$$
Lean4
/-- The core implementation of `Nat.repr` returns a String with length less than or equal to the
number of digits in the decimal number (represented by `e`). For example, the decimal string
representation of any number less than 1000 (10 ^ 3) has a length less than or equal to 3. -/
theorem repr_length (n e : Nat) : 0 < e → n < 10 ^ e → (Nat.repr n).length ≤ e :=
toDigits_length _ _ _
