toZ_iterate_succ

Mathlib.Order.SuccPred.LinearLocallyFinite

URI: https://scilib.ai/kg/mathlib#toZ_iterate_succ

English

The map i ↦ toZ i0 i is injective.

Русский

Отображение i ↦ toZ i0 i инъективно.

LaTeX

$$Function.Injective (toZ i_0)$$

Lean4

theorem toZ_iterate_succ [NoMaxOrder ι] (n : ℕ) : toZ i0 (succ^[n] i0) = n :=
  toZ_iterate_succ_of_not_isMax n (not_isMax _)

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

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

Разделы

Аффилиация

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