English
Let r be a binary relation on the natural numbers. The list range(n) is an r-chain if and only if r holds for every consecutive pair (m, m+1) with m < n−1.
Русский
Пусть r — бинарное отношение на натуральных числах. Последовательность range(n) образует цепь по отношению r тогда и только тогда, когда для каждого соседнего элемента пары (m, m+1) выполняется r m m+1 при m < n−1.
LaTeX
$$$\mathrm{IsChain}(r, \mathrm{range}(n)) \iff \forall m < n-1,\; r(m, m+1)$$$
Lean4
theorem isChain_range (r : ℕ → ℕ → Prop) (n : ℕ) : IsChain r (range n) ↔ ∀ m < n - 1, r m m.succ := by
induction n with
| zero => simp
| succ n hn =>
simp only [range_succ, Nat.add_one_sub_one, Nat.lt_sub_iff_add_lt] at hn ⊢
cases n with
| zero => simp
| succ
n =>
simp only [range_succ, Nat.add_lt_add_iff_right, succ_eq_add_one, append_assoc, cons_append, nil_append,
isChain_append_cons_cons, IsChain.singleton, and_true] at hn ⊢
rw [hn, forall_lt_succ_right]
