Def WithBot.subtypeOrderIso

Modification history

2026-04-05 08:48
Mathlib/Order/Hom/WithTopBot.lean
chore(Order/Hom/WithTopBot): use `to_dual` (#37274) …
Deleted WithBot.subtypeOrderIsoView on Github →
2025-08-14 03:55
Mathlib/Order/Hom/WithTopBot.lean
feat(Order): add {WithTop,WithBot}.subtypeOrderIso (#28192) …
Added WithBot.subtypeOrderIsoView on Github →