English
For the natural-number range, a chain property holds exactly when the relation relates consecutive indices and connects the end to the start.
Русский
Для диапазона натуральных чисел свойство цепи держится тогда и только тогда, когда связь между соседними индексами выполняется и соединение конца с началом выполняется.
LaTeX
$$$$ \\text{Chain } r (\\text{List.range }(n\\!+1)) \\iff r(n,0) \\wedge \\forall m < n, r(m, m\\!+1). $$$$
Lean4
theorem chain_range_succ (r : ℕ → ℕ → Prop) (n : ℕ) : Chain r (List.range n.succ) ↔ r n 0 ∧ ∀ m < n, r m m.succ := by
rw [range_succ, ← coe_cons_eq_coe_append, chain_coe_cons, ← range_succ, isChain_cons_range_succ]
