English
If r is decidable, then sorting with r implies sorting with the corresponding Boolean-valued relation decide(r a b) = true.
Русский
Если отношение r разрешимо (решаемо), то упорядоченность по r эквивалентна упорядоченности по булевой функции decide.
LaTeX
$$$$ \forall l:\text{List }\alpha,\ Sorted\ r\ l \Rightarrow \ Sorted (\lambda a b. (\operatorname{decide}(r\ a\ b) = \text{true}))\ l. $$$$
Lean4
/-- If a list is sorted with respect to a decidable relation,
then it is sorted with respect to the corresponding Bool-valued relation.
-/
theorem decide [DecidableRel r] (l : List α) (h : Sorted r l) : Sorted (fun a b => decide (r a b) = true) l := by
refine h.imp fun {a b} h => by simpa using h
