Theorem WithTop.coe_wcovBy_coe

Modification history

2024-08-23 15:37
Mathlib/Order/Cover.lean
feat(Order/Cover): add lemmas about `WithTop`/`WithBot` (#15487)
Added WithTop.coe_wcovBy_coeView on Github →