sorted_mergeSort' — Mathlib

English

Variant of sortedness of mergeSort using relation typeclasses: for l, the result mergeSort l is sorted w.r.t. r.

Русский

Вариант доказательства сортировки слиянием с использованием типовых классов: для списка l произведение mergeSort l упорядочено по r.

LaTeX

$$$ \\forall l, Sorted_r(\\text{mergeSort}(l)) $$$

Lean4

/-- Variant of `sorted_mergeSort` using relation typeclasses. -/
theorem sorted_mergeSort' (l : List α) : Sorted r (mergeSort l (r · ·)) := by
  simpa using sorted_mergeSort (le := (r · ·)) (fun _ _ _ => by simpa using trans_of r) (by simpa using total_of r) l

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