English
Let r be a relation on naturals. The list obtained by prepending a to range(n+1) is an r-chain exactly when r(a,0) holds and the rest of the range forms an r-chain: ∀ m < n, r(m, m+1).
Русский
Пусть r — отношение на натуральных. Сперва добавленная буква a к диапазону range(n+1) образует цепь по отношению r тогда и только тогда, когда r(a,0) выполняется и далее для всех m < n выполняется r(m, m+1).
LaTeX
$$$\mathrm{IsChain}(r, a :: \mathrm{range}(n.\mathrm{succ})) \iff r(a, 0) \land \forall m < n,\; r(m, m+1)$$$
Lean4
theorem isChain_cons_range_succ (r : ℕ → ℕ → Prop) (n a : ℕ) :
IsChain r (a :: range n.succ) ↔ r a 0 ∧ ∀ m < n, r m m.succ :=
by
rw [range_succ_eq_map, isChain_cons_cons, and_congr_right_iff, ← isChain_range_succ, range_succ_eq_map]
exact fun _ => Iff.rfl
