sorted_ge_ofFn_iff — Mathlib

English

The list produced by f is sorted with respect to ≥ iff f is Antitone.

Русский

Список, полученный из f, упорядочен по ≥ тогда, когда f — Antitone.

LaTeX

$$$$ (\text{List.Sorted } (\ge) (\text{List.ofFn } f)) \iff \text{Antitone } f. $$$$

Lean4

/-- The list `List.ofFn f` is sorted with respect to `(· ≥ ·)` if and only if `f` is antitone. -/
@[simp]
theorem sorted_ge_ofFn_iff : (ofFn f).Sorted (· ≥ ·) ↔ Antitone f :=
  sorted_ofFn_iff.trans antitone_iff_forall_lt.symm

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