Mathlib v3 is deprecated. Go to Mathlib v4

Def with_bot.order_iso_punit_sum_lex

Modification history

2022-07-21 02:26
src/data/sum/order.lean
feat(data/sum/order): `with_bot α ≃o punit ⊕ₗ α` and `with_top α ≃o α ⊕ₗ punit` (#15370)
Added with_bot.order_iso_punit_sum_lexView on Github →