sorted_le_ofFn_iff — Mathlib

English

For f: Fin n → α and a Preorder α, List.ofFn f is sorted by ≤ iff f is Monotone.

Русский

Для f: Fin n → α и предпорядка α список List.ofFn f упорядочен по ≤ тогда, когда f монотонна.

LaTeX

$$$$ (\text{List.Sorted } (\le) (\text{List.ofFn } f)) \iff \text{Monotone } f. $$$$

Lean4

/-- The list `List.ofFn f` is sorted with respect to `(· ≤ ·)` if and only if `f` is monotone. -/
@[simp]
theorem sorted_le_ofFn_iff : (ofFn f).Sorted (· ≤ ·) ↔ Monotone f :=
  sorted_ofFn_iff.trans monotone_iff_forall_lt.symm

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