Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-21 02:26 de04bafa

View on Github →

feat(data/sum/order): with_bot α ≃o punit ⊕ₗ α and with_top α ≃o α ⊕ₗ punit (#15370)

Estimated changes

Modified src/data/sum/order.lean

added def with_bot.order_iso_punit_sum_lex

added theorem with_bot.order_iso_punit_sum_lex_bot

added theorem with_bot.order_iso_punit_sum_lex_coe

added theorem with_bot.order_iso_punit_sum_lex_symm_inl

added theorem with_bot.order_iso_punit_sum_lex_symm_inr

added def with_top.order_iso_sum_lex_punit

added theorem with_top.order_iso_sum_lex_punit_coe

added theorem with_top.order_iso_sum_lex_punit_symm_inl

added theorem with_top.order_iso_sum_lex_punit_symm_inr

added theorem with_top.order_iso_sum_lex_punit_top