Commit 2024-06-15 07:07 04d5dcab

View on Github →

feat(Order): sup/inf equal to top/bot if top/bot in set (#13706) The sup lemma is needed in a proof related to SimpleGraph.ediam in #12058

Estimated changes

added theorem inf_eq_bot_of_bot_mem
added theorem sup_eq_top_of_top_mem