exists_succ_iterate_iff_le — Mathlib

English

In a Succ-Archimedean preorder, there exists n with succ-iterate equals b from a iff a ≤ b.

Русский

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

LaTeX

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

Lean4

theorem exists_succ_iterate_iff_le : (∃ n, succ^[n] a = b) ↔ a ≤ b :=
  by
  refine ⟨?_, exists_succ_iterate_of_le⟩
  rintro ⟨n, rfl⟩
  exact id_le_iterate_of_id_le le_succ n a

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