Theorem max_eq_top

Modification history

2025-12-26 18:30

Mathlib/Order/BoundedOrder/Lattice.lean

refactor(Order/BoundedOrder/Lattice): use `to_dual` (#33268) …

Deleted max_eq_top View on Github →

2024-11-26 05:23

Mathlib/Order/BoundedOrder/Basic.lean

chore: split Order.BoundedOrder (#19488)

Modified max_eq_top View on Github →

2022-11-28 15:54

Mathlib/Order/BoundedOrder.lean

feat: port Order.BoundedOrder (#697) …

Added max_eq_top View on Github →