English
If r is a transitive relation on β, and f: ℕ → β satisfies r(f n) (f(n+1)) for all n beyond a, then for any b<c with a ≤ b < c, r(f b) (f c).
Русский
Пусть r — транзитивное отношение на β, и f: ℕ → β удовлетворяет r(f n) (f(n+1)) для всех n ≥ a. Тогда при любых b < c с a ≤ b выполняется r(f b) (f c).
LaTeX
$$$ (r : β \to β \to Prop) [IsTrans β r] [IsTrans β r] {f : ℕ \to β} {a : ℕ} (h : \forall n, a \le n \rightarrow r (f n) (f (n + 1))) ⦃b c : ℕ⦄ (hab : a \le b) (hbc : b < c) : r (f b) (f c) $$$
Lean4
theorem rel_of_forall_rel_succ_of_le_of_lt (r : β → β → Prop) [IsTrans β r] {f : ℕ → β} {a : ℕ}
(h : ∀ n, a ≤ n → r (f n) (f (n + 1))) ⦃b c : ℕ⦄ (hab : a ≤ b) (hbc : b < c) : r (f b) (f c) := by
induction hbc with
| refl => exact h _ hab
| step b_lt_k r_b_k => exact _root_.trans r_b_k (h _ (hab.trans_lt b_lt_k).le)
