Equal neighbors in monotone finite arrays

A repeated value in a monotone finite array has an equal predecessor or successor. The value type needs only a partial order.

Main results

• Fin.exists_ne_apply_eq_iff_adjacent: an adjacent witness suffices for any repeated value.

References

Adapted from MassProduction/Nonuniform/AdjacentDuplicates.lean in S. Schlesinger, Boolean circuit mass production formalization.

theorem Fin.exists_ne_apply_eq_iff_adjacent {α : Type u_1} [PartialOrder α] {count : ℕ} (f : Fin count → α) (ordered : Monotone f) (i : Fin count) : (∃ (j : Fin count), j ≠ i ∧ f j = f i) ↔ (∃ (positive : 0 < ↑i), f ⟨↑i - 1, ⋯⟩ = f i) ∨ ∃ (fits : ↑i + 1 < count), f ⟨↑i + 1, fits⟩ = f i

In a monotone finite array, every repeated value has an equal neighbor.