Theorem WithTop.subtypeOrderIso_apply_coe

Modification history

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