English
If r is reflexive and transitive on β, and f: ℕ → β satisfies r(f(n), f(n+1)) for all n, then for any a ≤ b, 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{IsRefl} β\, r] [\\mathrm{IsTrans} β\, r] {f : \\mathbb{N} \\to β} (h : \\forall n, r (f n) (f (n + 1))) \\; \\forall a b : \\mathbb{N}, a \\le b \\Rightarrow r (f a) (f b)$$$
Lean4
theorem rel_of_forall_rel_succ_of_le (r : β → β → Prop) [IsRefl β r] [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_le r (fun n _ ↦ h n) le_rfl hab
