English
Let r be a transitive relation on β. Let f: ℕ → β satisfy r(f(n), f(n+1)) for all n. Then for any a,b ∈ ℕ with a < b, r(f(a), f(b)).
Русский
Пусть r — транзитивное отношение на β. Пусть f: ℕ → β удовлетворяет r(f(n), f(n+1)) для всех n. Тогда для любых a, b ∈ ℕ с a < b выполняется r(f(a), f(b)).
LaTeX
$$$\\forall (r : \\beta \\to β \\to \\mathrm{Prop}) [\\mathrm{IsTrans} β\, r] {f : \\mathbb{N} \\to β} (h : \\forall n, r (f n) (f (n + 1))) \\; \\forall a b : \\mathbb{N}, 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) :=
Nat.rel_of_forall_rel_succ_of_le_of_lt r (fun n _ ↦ h n) le_rfl hab
