Theorem WithTop.lt_iff_exists

Modification history

2025-11-03 16:36
Mathlib/Order/WithBot.lean
refactor: define `<` on `WithBot`/`WithTop` as an inductive predicate (#30848) …
Added WithTop.lt_iff_existsView on Github →