Commit 2024-01-23 09:49 2475f305

View on Github →

feat(Order/WithBot): add WithBot.lt_coe_bot (#9898)

  • Add WithBot.lt_coe_bot and WithTop.coe_top_lt.
  • Use them to golf Nat.WithBot.lt_zero_iff, make n argument implicit.
  • Add section Preorder for WithBot and WithTop.
  • Move some lemmas to appropriate sections.
  • Add simp to WithBot.bot_lt_coe and WithTop.coe_lt_top.
  • Use the OrderDual trick to golf some proofs.

Estimated changes

modified theorem Nat.WithBot.lt_zero_iff
modified theorem WithBot.coe_mono
modified theorem WithBot.coe_strictMono
modified theorem WithBot.le_coe_unbot'
added theorem WithBot.lt_coe_bot
modified theorem WithBot.map_le_iff
modified theorem WithBot.monotone_iff
modified theorem WithBot.monotone_map_iff
modified theorem WithBot.strictAnti_iff
modified theorem WithBot.strictMono_iff
modified theorem WithBot.strictMono_map_iff
modified theorem WithBot.unbot'_le_iff
modified theorem WithBot.unbot'_lt_iff
modified theorem WithTop.coe_mono
modified theorem WithTop.coe_strictMono
added theorem WithTop.coe_top_lt
modified theorem WithTop.coe_untop'_le
modified theorem WithTop.le_untop'_iff
modified theorem WithTop.lt_untop'_iff
modified theorem WithTop.map_le_iff
modified theorem WithTop.monotone_iff
modified theorem WithTop.monotone_map_iff
modified theorem WithTop.strictAnti_iff
modified theorem WithTop.strictMono_iff
modified theorem WithTop.strictMono_map_iff