English
For any n, α, f: Fin n → α, and any relation r, the list of values f is r-sorted iff f is strictly monotone with respect to r.
Русский
Для функции f: Fin n → α список List.ofFn f упорядочен по r тогда, когда f строго монотонна относительно r.
LaTeX
$$$$ \forall n:\mathbb{N},\forall \alpha,\forall f:\text{Fin } n \to \alpha,\forall r: \alpha \to \alpha \to \text{Prop},\ (\text{List.Sorted } r (\text{List.ofFn } f)) \iff \Big(\forall i j: \text{Fin } n,\ i < j \Rightarrow r (f i) (f j)\Big). $$$$
Lean4
theorem sorted_ofFn_iff {r : α → α → Prop} : (ofFn f).Sorted r ↔ ((· < ·) ⇒ r) f f :=
by
simp_rw [Sorted, pairwise_iff_get, get_ofFn, Relator.LiftFun]
exact Iff.symm (Fin.rightInverse_cast _).surjective.forall₂
