English
Let r be a transitive relation on β, and f: ℤ → β such that r(f(n), f(n+1)) for all n. Then for any a < b in ℤ, r(f(a), f(b)).
Русский
Пусть r — транзитивное отношение на β, и f: ℤ → β удовлетворяет r(f(n), f(n+1)) для всех n. Тогда для любых a < b в ℤ верно r(f(a), f(b)).
LaTeX
$$$\\forall (r : β \\to β \\to \\mathrm{Prop}) [\\mathrm{IsTrans} β\\ r] {f : \\mathbb{Z} \\to β} (h : \\forall n, r (f n) (f (n + 1))) \\; \\forall a b : \\mathbb{Z}, a < b \\Rightarrow r (f a) (f b)$$$
Lean4
theorem rel_of_forall_rel_succ_of_lt (r : β → β → Prop) [IsTrans β r] {f : ℤ → β} (h : ∀ n, r (f n) (f (n + 1)))
⦃a b : ℤ⦄ (hab : a < b) : r (f a) (f b) :=
by
rcases lt.dest hab with ⟨n, rfl⟩
clear hab
induction n with
| zero => rw [Int.ofNat_one]; apply h
| succ n ihn => rw [Int.natCast_succ, ← Int.add_assoc]; exact _root_.trans ihn (h _)
