Commit 2021-01-03 02:24 9f252442

View on Github →

chore(data/finset/sort): upgrade finset.mono_of_fin to an order_iso (#5495)

  • Upgrade finset.mono_of_fin to an order_embedding.
  • Drop some lemmas that now immediately follow from order_embedding.*.
  • Upgrade finset.mono_equiv_of_fin to order_iso.
  • Define list.nodup.nth_le_equiv and list.sorted.nth_le_iso.
  • Upgrade mono_equiv_of_fin to an order_iso, make it computable.

Estimated changes