isChain_ofFn — Mathlib

English

For a finite index type Fin n, the list of values f(i) forms a chain with respect to R if and only if adjacent values satisfy R.

Русский

Для финитной индексации Fin n список значений f(i) образуют цепь по отношению R тогда и только тогда, когда соседние значения удовлетворяют R.

LaTeX

$$$(\\text{List.ofFn } f)\\ IsChain\\ R\\iff\\ \\forall i, (i+1

Lean4

theorem isChain_ofFn {α : Type*} {n : ℕ} {f : Fin n → α} {r : α → α → Prop} :
    (ofFn f).IsChain r ↔ ∀ (i) (hi : i + 1 < n), r (f ⟨i, lt_of_succ_lt hi⟩) (f ⟨i + 1, hi⟩) :=
  by
  simp_rw [isChain_iff_get, get_ofFn, length_ofFn]
  exact ⟨fun h i hi ↦ h i (by cutsat), fun h i hi ↦ h i (by cutsat)⟩

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