Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-15 23:11 091ccfb2

View on Github →

feat(order/bounded_order): with_top.of_dual (#15727) with_top.to_dual : with_top α ≃ with_bot αᵒᵈ Also define

  • with_top.of_dual
  • with_bot.to_dual
  • with_bot.of_dual

API on the application of these added, their relation to le and lt, and how they interact with with_{bot,top}.map

Some with_top proofs that broke through the option or order_dual API have been rephrased to carry over the with_bot proofs across these functions.

Estimated changes

added theorem with_bot.map_of_dual
added theorem with_bot.map_to_dual
added theorem with_bot.of_dual_map
added theorem with_bot.to_dual_map
modified theorem with_top.coe_le_coe
modified theorem with_top.coe_le_iff
modified theorem with_top.coe_lt_coe
modified theorem with_top.coe_lt_iff
modified theorem with_top.coe_lt_top
modified theorem with_top.le_coe_iff
modified theorem with_top.lt_iff_exists_coe
added theorem with_top.map_of_dual
added theorem with_top.map_to_dual
added theorem with_top.of_dual_map
modified theorem with_top.some_le_some
modified theorem with_top.some_lt_none
modified theorem with_top.some_lt_some
added theorem with_top.to_dual_map
deleted theorem with_bot.to_dual_top_coe
deleted theorem with_top.to_dual_bot_coe