Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-28 13:31 ff241e13

View on Github →

feat(order/max): Predicate for minimal/maximal elements, typeclass for orders without bottoms (#11618) This defines

  • is_min: Predicate for a minimal element
  • is_max: Predicate for a maximal element
  • no_bot_order: Predicate for an order without bottoms
  • no_top_order: Predicate for an order without tops

Estimated changes

added theorem is_bot_iff_is_min
added theorem is_top_iff_is_max
added theorem is_bot.mono
deleted theorem is_bot.to_dual
added theorem is_bot_of_dual_iff
added theorem is_bot_to_dual_iff
added theorem is_max.mono
added theorem is_max.not_lt
added def is_max
added theorem is_max_of_dual_iff
added theorem is_max_to_dual_iff
added theorem is_min.mono
added theorem is_min.not_lt
added def is_min
added theorem is_min_of_dual_iff
added theorem is_min_to_dual_iff
added theorem is_top.mono
deleted theorem is_top.to_dual
modified theorem is_top.unique
added theorem is_top_of_dual_iff
added theorem is_top_to_dual_iff
modified theorem not_is_bot
added theorem not_is_max
added theorem not_is_max_iff
added theorem not_is_min
added theorem not_is_min_iff
modified theorem not_is_top