Theorem WithTop.le_coe_iff

Modification history

2025-12-18 23:55
Mathlib/Order/WithBot.lean
chore(Order/WithBot): add to_dual attributes (part 2) (#32626) …
Deleted WithTop.le_coe_iffView on Github →
2025-10-16 16:35
Mathlib/Order/WithBot.lean
refactor: define `≤`/`<` on `WithBot`/`WithTop` by induction (#19668) …
Modified WithTop.le_coe_iffView on Github →
2025-02-12 11:53
Mathlib/Order/WithBot.lean
chore(Order/WithBot): golf, clean up (#21274) …
Modified WithTop.le_coe_iffView on Github →
2022-11-29 20:56
Mathlib/Order/WithBot.lean
feat: port Order.WithBot (#777) …
Added WithTop.le_coe_iffView on Github →