Commit 2021-11-29 09:57 957fa4bb

View on Github →

feat(order/locally_finite): with_top α/with_bot α are locally finite orders (#10202) This provides the two instances locally_finite_order (with_top α) and locally_finite_order (with_bot α).

Estimated changes

Modified src/data/finset/basic.lean

added theorem finset.mem_cons_self

Modified src/data/option/defs.lean

added theorem option.mem_iff

Modified src/logic/embedding.lean

added def function.embedding.coe_option

added def function.embedding.coe_with_top

Modified src/order/locally_finite.lean

added theorem with_bot.Icc_bot_coe

added theorem with_bot.Icc_coe_coe

added theorem with_bot.Ico_bot_coe

added theorem with_bot.Ico_coe_coe

added theorem with_bot.Ioc_bot_coe

added theorem with_bot.Ioc_coe_coe

added theorem with_bot.Ioo_bot_coe

added theorem with_bot.Ioo_coe_coe

added theorem with_top.Icc_coe_coe

added theorem with_top.Icc_coe_top

added theorem with_top.Ico_coe_coe

added theorem with_top.Ico_coe_top

added theorem with_top.Ioc_coe_coe

added theorem with_top.Ioc_coe_top

added theorem with_top.Ioo_coe_coe

added theorem with_top.Ioo_coe_top