injective

Mathlib.Data.Nat.Digits.Defs

URI: https://scilib.ai/kg/mathlib#Nat.digits.injective

English

For every base b, the function n ↦ digits_b(n) is injective.

Русский

Для любой базы b функция n ↦ digits_b(n) инъективна.

LaTeX

$$$ \forall b\in\mathbb{N},\ \mathrm{Injective}(\mathrm{digits}_b) $$$

Lean4

theorem injective (b : ℕ) : Function.Injective b.digits :=
  Function.LeftInverse.injective (ofDigits_digits b)

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

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

Разделы

Аффилиация

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