Theorem max_ne_top

Modification history

2025-12-26 18:30
Mathlib/Order/BoundedOrder/Lattice.lean
refactor(Order/BoundedOrder/Lattice): use `to_dual` (#33268) …
Deleted max_ne_topView on Github →
2025-05-27 14:09
Mathlib/Order/BoundedOrder/Lattice.lean
feat(Tactic/Finiteness): tag more lemmas (#25086) …
Added max_ne_topView on Github →