Mathlib v3 is deprecated. Go to Mathlib v4

Theorem with_bot.order_iso_punit_sum_lex_coe

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_lex_coe View on Github →