Theorems · Theorem · order theory

Finset.sort_mk

∀ {α : Type u_1} {m : Multiset α} (r : α → α → Prop) [inst : DecidableRel r] [inst_1 : IsTrans α r]
  [inst_2 : Std.Antisymm r] [inst_3 : Std.Total r] (h : m.Nodup), { val := m, nodup := h }.sort r = m.sort r

Defined in

Mathlib.Data.Finset.Sort

Cited by

0 results in Mathlib

Foundations

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

Assumes

DecidableRelIsTransStd.AntisymmStd.Total