Commit 2023-01-26 07:43 02346994

View on Github →

feat: port Order.LocallyFinite (#1754)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/LocallyFinite.lean

added def Finset.Icc

added def Finset.Ici

added theorem Finset.Ici_eq_Icc

added def Finset.Ico

added def Finset.Iic

added theorem Finset.Iic_eq_Icc

added def Finset.Iio

added theorem Finset.Iio_eq_Ico

added def Finset.Ioc

added def Finset.Ioi

added theorem Finset.Ioi_eq_Ioc

added def Finset.Ioo

added theorem Finset.coe_Icc

added theorem Finset.coe_Ici

added theorem Finset.coe_Ico

added theorem Finset.coe_Iic

added theorem Finset.coe_Iio

added theorem Finset.coe_Ioc

added theorem Finset.coe_Ioi

added theorem Finset.coe_Ioo

added theorem Finset.coe_uIcc

added theorem Finset.map_subtype_embedding_Icc

added theorem Finset.map_subtype_embedding_Ici

added theorem Finset.map_subtype_embedding_Ico

added theorem Finset.map_subtype_embedding_Iic

added theorem Finset.map_subtype_embedding_Iio

added theorem Finset.map_subtype_embedding_Ioc

added theorem Finset.map_subtype_embedding_Ioi

added theorem Finset.map_subtype_embedding_Ioo

added theorem Finset.mem_Icc

added theorem Finset.mem_Ici

added theorem Finset.mem_Ico

added theorem Finset.mem_Iic

added theorem Finset.mem_Iio

added theorem Finset.mem_Ioc

added theorem Finset.mem_Ioi

added theorem Finset.mem_Ioo

added theorem Finset.mem_uIcc

added theorem Finset.subtype_Icc_eq

added theorem Finset.subtype_Ici_eq

added theorem Finset.subtype_Ico_eq

added theorem Finset.subtype_Iic_eq

added theorem Finset.subtype_Iio_eq

added theorem Finset.subtype_Ioc_eq

added theorem Finset.subtype_Ioi_eq

added theorem Finset.subtype_Ioo_eq

added def Finset.uIcc

added def Fintype.toLocallyFiniteOrder

added theorem Icc_ofDual

added theorem Icc_toDual

added theorem Ici_ofDual

added theorem Ici_toDual

added theorem Ico_ofDual

added theorem Ico_toDual

added theorem Iic_ofDual

added theorem Iic_toDual

added theorem Iio_ofDual

added theorem Iio_toDual

added theorem Ioc_ofDual

added theorem Ioc_toDual

added theorem Ioi_ofDual

added theorem Ioi_toDual

added theorem Ioo_ofDual

added theorem Ioo_toDual

added def LocallyFiniteOrder.ofIcc'

added def LocallyFiniteOrder.ofIcc

added def LocallyFiniteOrderBot.ofIic'

added def LocallyFiniteOrderTop.ofIci'

added def LocallyFiniteOrderTop.ofIci

added def LocallyFiniteOrderTop.ofIic

added def Multiset.Icc

added def Multiset.Ici

added def Multiset.Ico

added def Multiset.Iic

added def Multiset.Iio

added def Multiset.Ioc

added def Multiset.Ioi

added def Multiset.Ioo

added theorem Multiset.mem_Icc

added theorem Multiset.mem_Ici

added theorem Multiset.mem_Ico

added theorem Multiset.mem_Iic

added theorem Multiset.mem_Iio

added theorem Multiset.mem_Ioc

added theorem Multiset.mem_Ioi

added theorem Multiset.mem_Ioo

added def OrderIso.locallyFiniteOrder

added def OrderIso.locallyFiniteOrderBot

added def OrderIso.locallyFiniteOrderTop

added theorem Prod.Icc_eq

added theorem Prod.Icc_mk_mk

added theorem Prod.card_Icc

added theorem Prod.card_uIcc

added theorem Prod.uIcc_eq

added theorem Prod.uIcc_mk_mk

added theorem Set.finite_Icc

added theorem Set.finite_Ici

added theorem Set.finite_Ico

added theorem Set.finite_Iic

added theorem Set.finite_Iio

added theorem Set.finite_Ioc

added theorem Set.finite_Ioi

added theorem Set.finite_Ioo

added theorem WithBot.Icc_bot_coe

added theorem WithBot.Icc_coe_coe

added theorem WithBot.Ico_bot_coe

added theorem WithBot.Ico_coe_coe

added theorem WithBot.Ioc_bot_coe

added theorem WithBot.Ioc_coe_coe

added theorem WithBot.Ioo_bot_coe

added theorem WithBot.Ioo_coe_coe

added theorem WithTop.Icc_coe_coe

added theorem WithTop.Icc_coe_top

added theorem WithTop.Ico_coe_coe

added theorem WithTop.Ico_coe_top

added theorem WithTop.Ioc_coe_coe

added theorem WithTop.Ioc_coe_top

added theorem WithTop.Ioo_coe_coe

added theorem WithTop.Ioo_coe_top