English
Let r be a reflexive and transitive relation on β, and f: ℕ → β with h: ∀ n, a ≤ n → r (f n) (f (n+1)). Then for any b ≤ c with a ≤ b, r (f b) (f c) holds.
Русский
Пусть r рефлексивно и транзитивно на β, и f: ℕ → β с условием h: ∀ n, a ≤ n → r (f n) (f (n+1)). Тогда для любых b ≤ c с a ≤ b выполняется r (f b) (f c).
LaTeX
$$$ (r : β \to β \to Prop) [IsRefl β r] [IsTrans β r] {f : ℕ \to β} {a : ℕ} (h : ∀ n, a \le n → r (f n) (f (n + 1))) ⦃b c : ℕ⦄ (hab : a \le b) (hbc : b \le c) : r (f b) (f c) $$$
Lean4
theorem rel_of_forall_rel_succ_of_le_of_le (r : β → β → Prop) [IsRefl β r] [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) :=
hbc.eq_or_lt.elim (fun h ↦ h ▸ refl _) (Nat.rel_of_forall_rel_succ_of_le_of_lt r h hab)
