Theorem WithTop.le_iff_forall

Modification history

2025-10-16 16:35
Mathlib/Order/WithBot.lean
refactor: define `≤`/`<` on `WithBot`/`WithTop` by induction (#19668) …
Added WithTop.le_iff_forallView on Github →