Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-05 13:15 8b913902

View on Github →

feat(order/hom/basic): add order_iso.with_{top,bot}_congr (#12264) This adds:

  • with_bot.to_dual_top
  • with_top.to_dual_bot
  • order_iso.with_top_congr
  • order_iso.with_bot_congr

Estimated changes

added theorem option.map_coe'
added theorem option.map_coe
added theorem with_bot.map_bot
added theorem with_bot.map_coe
added theorem with_top.map_coe
added theorem with_top.map_top