Theorem WithTop.lt_def

Modification history

2025-12-18 23:55
Mathlib/Order/WithBot.lean
chore(Order/WithBot): add to_dual attributes (part 2) (#32626) …
Modified WithTop.lt_defView on Github →
2025-11-03 16:36
Mathlib/Order/WithBot.lean
refactor: define `<` on `WithBot`/`WithTop` as an inductive predicate (#30848) …
Modified WithTop.lt_defView on Github →
2025-10-16 16:35
Mathlib/Order/WithBot.lean
refactor: define `≤`/`<` on `WithBot`/`WithTop` by induction (#19668) …
Modified WithTop.lt_defView on Github →
2025-02-12 11:53
Mathlib/Order/WithBot.lean
chore(Order/WithBot): golf, clean up (#21274) …
Added WithTop.lt_defView on Github →