Theorems · Theorem · combinatorics

Multiset.map_sort

∀ {α : Type u_1} {β : Type u_2} (f : α → β) (s : Multiset α) (r : α → α → Prop) [inst : DecidableRel r]
  [inst_1 : IsTrans α r] [inst_2 : Std.Antisymm r] [inst_3 : Std.Total r] (r' : β → β → Prop) [inst_4 : DecidableRel r']
  [inst_5 : IsTrans β r'] [inst_6 : Std.Antisymm r'] [inst_7 : Std.Total r'],
  (∀ a ∈ s, ∀ b ∈ s, r a b ↔ r' (f a) (f b)) → List.map f (s.sort r) = (Multiset.map f s).sort r'

Defined in

Mathlib.Data.Multiset.Sort

Cited by

1 results in Mathlib

Foundations

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

Assumes

DecidableRelIsTransStd.AntisymmStd.TotalDecidableRelIsTransStd.AntisymmStd.Total