Def WithTop.subtypeOrderIso

Modification history

2025-08-14 03:55
Mathlib/Order/Hom/WithTopBot.lean
feat(Order): add {WithTop,WithBot}.subtypeOrderIso (#28192) …
Added WithTop.subtypeOrderIsoView on Github →