Theorem WithTop.subtypeOrderIso_symm_apply

Modification history

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