le_digits_len_le

Mathlib.Data.Nat.Digits.Lemmas

URI: https://scilib.ai/kg/mathlib#Nat.le_digits_len_le

← MathLib Explorer

English

For base b and n, (digits b n).length ≤ (digits b (n+1)).length.

Русский

Для основания b и n: длина digits b n не превосходит длину digits b (n+1).

LaTeX

$$$\\forall b,n:\\; (digits\\ b\\ n).length ≤ (digits\\ b\\ (n+1)).length$$$

Lean4

theorem le_digits_len_le (b n m : ℕ) (h : n ≤ m) : (digits b n).length ≤ (digits b m).length :=
  monotone_nat_of_le_succ (digits_len_le_digits_len_succ b) h

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru