Theorems · Theorem · combinatorics

Multiset.pairwise_sort

∀ {α : Type u_1} (s : Multiset α) (r : α → α → Prop) [inst : DecidableRel r] [inst_1 : IsTrans α r]
  [inst_2 : Std.Antisymm r] [inst_3 : Std.Total r], List.Pairwise r (s.sort r)

Defined in

Mathlib.Data.Multiset.Sort

Cited by

2 results in Mathlib

Foundations

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

Assumes

DecidableRelIsTransStd.AntisymmStd.Total