Theorem sup_eq_top_of_top_mem

Modification history

2026-02-16 16:43
Mathlib/Order/ConditionallyCompleteLattice/Basic.lean
feat: basic API for `ConditionallyCompletePartialOrder` (#35047) …
Modified sup_eq_top_of_top_memView on Github →
2024-06-15 07:07
Mathlib/Order/ConditionallyCompleteLattice/Basic.lean
feat(Order): sup/inf equal to top/bot if top/bot in set (#13706) …
Added sup_eq_top_of_top_memView on Github →