exists_succ_iterate

Mathlib.Order.SuccPred.Archimedean

URI: https://scilib.ai/kg/mathlib#LE.le.exists_succ_iterate

English

If a ≤ b in a Succ-Archimedean preorder, then there exists n with b = a after n steps of succ.

Русский

Если a ≤ b в пределе с Succ-Archimedean, то существует n, такое что b достигается из a за n шагов succ.

LaTeX

$$$a \le b \Rightarrow \exists n, (\mathrm{succ})^{[n]}(a) = b$$$

Lean4

theorem exists_succ_iterate (h : a ≤ b) : ∃ n, succ^[n] a = b :=
  exists_succ_iterate_of_le h

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

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

Разделы

Аффилиация

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