sorted_gt_ofFn_iff — Mathlib

English

For fin n and f: Fin n → α, List.ofFn f is sorted by > iff f is StrictAnti.

Русский

Для конечного n и функции f: Fin n → α, List.ofFn f упорядочен по > тогда, когда f является StrictAnti.

LaTeX

$$$$ (\text{List.Sorted } (\gt) (\text{List.ofFn } f)) \iff \text{StrictAnti } f. $$$$

Lean4

/-- The list `List.ofFn f` is strictly sorted with respect to `(· ≥ ·)` if and only if `f` is
strictly antitone. -/
@[simp]
theorem sorted_gt_ofFn_iff : (ofFn f).Sorted (· > ·) ↔ StrictAnti f :=
  sorted_ofFn_iff

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