isChain_succ — Mathlib

English

The list Ico n m forms a chain where each element is the successor of the previous one.

Русский

Список Ico n m образует цепочку: каждый следующий элемент является преемником предыдущего.

LaTeX

$$$\operatorname{IsChain}(\lambda a,b.\ b = a+1)(\operatorname{Ico}(n,m))$$$

Lean4

theorem isChain_succ (n m : ℕ) : IsChain (fun a b => b = succ a) (Ico n m) :=
  by
  by_cases h : n < m
  · rw [eq_cons h]
    unfold List.Ico
    exact isChain_range' _ (_ + 1) 1
  · rw [eq_nil_of_le (le_of_not_gt h)]
    exact .nil

Похожие утверждения