Lemmas about IsChain and ofFn

This file provides lemmas involving both List.IsChain and List.ofFn.

theorem List.isChain_ofFn {α : Type u_1} {n : ℕ} {f : Fin n → α} {r : α → α → Prop} : IsChain r (ofFn f) ↔ ∀ (i : ℕ) (hi : i + 1 < n), r (f ⟨i, ⋯⟩) (f ⟨i + 1, hi⟩)

@[deprecated List.isChain_ofFn (since := "2025-09-24")]

theorem List.chain'_ofFn {α : Type u_1} {n : ℕ} {f : Fin n → α} {r : α → α → Prop} : IsChain r (ofFn f) ↔ ∀ (i : ℕ) (hi : i + 1 < n), r (f ⟨i, ⋯⟩) (f ⟨i + 1, hi⟩)

Alias of List.isChain_ofFn.