Theorems · Theorem · combinatorics

Multiset.sort_cons

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

Defined in

Mathlib.Data.Multiset.Sort

Cited by

1 results in Mathlib

Foundations

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

Assumes

DecidableRelIsTransStd.AntisymmStd.Total