Sorting is injective

Stream: Is there code for X?

[Yaël Dillies]

Do we have the fact that sorting is injective, in any form? The precise statement I'm interested in is

import data.multiset.sort

open function multiset

variables {α : Type*} {r : α → α → Prop} [decidable_rel r] [is_trans α r] [is_antisymm α r] [is_total α r]

lemma multiset.sort_injective : injective (sort r) := sorry

[Adam Topaz]

import data.multiset.sort

open function multiset

variables {α : Type*} {r : α → α → Prop} [decidable_rel r] [is_trans α r] [is_antisymm α r] [is_total α r]

lemma multiset.sort_injective : injective (sort r) :=
λ x y h, by simpa using congr_arg (coe : list α → multiset α) h

Is it worth it to have this as a lemma?

[Yaël Dillies]

It would certainly be useful to me! I am defining majorization as a relation multiset α → multiset α → Prop and this allows me to prove that it's antisymmetric.

[Adam Topaz]

I guess having a left inverse lemma does make sense

lemma multiset.left_inverse_coe_sort :
  function.left_inverse coe (sort r) :=
λ a, by simp

lemma multiset.sort_injective : injective (sort r) :=
multiset.left_inverse_coe_sort.injective

[Jireh Loreaux]

What notion of majorization are you defining? I have a lot of background in this area.

[Yaël Dillies]

This is my definition

import algebra.big_operators.basic
import data.multiset.sort

def weak_majorize (s t : multiset α) : Prop :=
s.card = t.card ∧ ∀ n, ((s.sort (≥)).take n).sum ≤ ((t.sort (≥)).take n).sum

infix ` ≼ʷ `:50 := weak_majorize

def majorize (s t : multiset α) : Prop := s ≼ʷ t ∧ s.sum = t.sum

infix ` ≼ᵐ `:50 := majorize

def strict_majorize (s t : multiset α) : Prop := s ≼ᵐ t ∧ ¬ t ≼ᵐ s

infix ` ≺ᵐ `:50 := strict_majorize