English
Let α be a preorder with successors and Archimedean property. If p(a) ↔ p(succ a) for all a, then for all a ≤ b, p(a) ↔ p(b).
Русский
Пусть α — частичноупорядоченное множество с переходами-кандидатами и архимедовым свойством. Если p(a) ⇔ p(следующий a) для всех a, тогда при любых a ≤ b имеем p(a) ⇔ p(b).
LaTeX
$$$( \forall a, p(a) \leftrightarrow p(\mathrm{succ}(a)) ) \rightarrow ( \forall a,b, a \le b \rightarrow p(a) \leftrightarrow p(b) )$$$
Lean4
theorem rec_iff {p : α → Prop} (hsucc : ∀ a, p a ↔ p (succ a)) {a b : α} (h : a ≤ b) : p a ↔ p b :=
by
obtain ⟨n, rfl⟩ := h.exists_succ_iterate
exact Iterate.rec (fun b => p a ↔ p b) Iff.rfl (fun c hc => hc.trans (hsucc _)) n
