sorted_lt_ofFn_iff — Mathlib

English

The list of values f on Fin n is strictly sorted by < if and only if f is strictly monotone.

Русский

Последовательность значений функции f на Fin(n) строго возрастает по отношению к < тогда и только тогда, когда f строго монотонна.

LaTeX

$$$(\\mathrm{ofFn}(f)).\\mathrm{Sorted}(<) \\iff \\mathrm{StrictMono}(f)$$$

Lean4

/-- The list `List.ofFn f` is strictly sorted with respect to `(· ≤ ·)` if and only if `f` is
strictly monotone. -/
@[simp]
theorem sorted_lt_ofFn_iff : (ofFn f).Sorted (· < ·) ↔ StrictMono f :=
  sorted_ofFn_iff

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