Theorems · Theorem · order theory

List.mergeSort_eq_self

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

Defined in

Mathlib.Data.List.Sort

Cited by

1 results in Mathlib

Foundations

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

Assumes

DecidableRelStd.TotalIsTransStd.Antisymm