Commit 2025-08-14 03:55 f0a0e4da

View on Github →

feat(Order): add {WithTop,WithBot}.subtypeOrderIso (#28192) Separated from #25970

Estimated changes

Modified Mathlib/Order/Hom/WithTopBot.lean

added def WithBot.subtypeOrderIso

added theorem WithBot.subtypeOrderIso_apply_coe

added theorem WithBot.subtypeOrderIso_symm_apply

added def WithTop.subtypeOrderIso

added theorem WithTop.subtypeOrderIso_apply_coe

added theorem WithTop.subtypeOrderIso_symm_apply