Theorems · Theorem · order theory

List.mergeSort_eq_insertionSort

∀ {α : Type u_1} (r : α → α → Prop) [inst : DecidableRel r] [Std.Total r] [IsTrans α r] [Std.Antisymm r] (l : List α),
  (l.mergeSort fun x1 x2 => decide (r x1 x2)) = List.insertionSort r l

Defined in

Mathlib.Data.List.Sort

Cited by

1 results in Mathlib

Foundations

Depth 58 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DecidableRelStd.TotalIsTransStd.Antisymm