isChain_range_succ — Mathlib

English

Let r be a binary relation on the natural numbers. The list range(n+1) is an r-chain if and only if r holds for every consecutive pair (m, m+1) with m < n.

Русский

Пусть r — бинарное отношение на натуральных числах. Последовательность range(n+1) образует цепь по отношению r тогда и только тогда, когда для каждого соседнего элемента пары (m, m+1) выполняется r m m+1 при m < n.

LaTeX

$$$\mathrm{IsChain}(r, \mathrm{range}(n.\mathrm{succ})) \iff \forall m < n,\; r(m, m+1)$$$

Lean4

theorem isChain_range_succ (r : ℕ → ℕ → Prop) (n : ℕ) : IsChain r (range n.succ) ↔ ∀ m < n, r m m.succ := by
  rw [isChain_range, succ_eq_add_one, Nat.add_one_sub_one]

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