Mathlib v3 is deprecated. Go to Mathlib v4

Theorem with_top.order_iso_sum_lex_punit_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_top.order_iso_sum_lex_punit_coe View on Github →