List.sort

Stream: Is there code for X?

[Violeta Hernández]

I do know docs#List.mergeSort exists, so my question isn't that but rather: is that the preferred spelling for talking about sorting a list?

[Violeta Hernández]

Oops, this might have been an #XY. Just found about docs#Finset.sort

[Violeta Hernández]

Another question. Do we have l.toFinset.toList ~ l for Nodup l?

[Daniel Weber]

@loogle List.Nodup, List.toFinset

[loogle]

:search: List.toFinset_eq, Finset.exists_list_nodup_eq, and 14 more

[Daniel Weber]

This should be immediate from docs#List.perm_of_nodup_nodup_toFinset_eq

[Violeta Hernández]

Indeed

import Mathlib.Data.Finset.Basic

theorem List.toFinset_toList [DecidableEq α] {s : List α} (hs : s.Nodup) :
    s.toFinset.toList.Perm s :=
  List.perm_of_nodup_nodup_toFinset_eq (Finset.nodup_toList _) hs (Finset.toList_toFinset _)