Commit 2023-01-26 10:01 e2c39a45

View on Github →

feat: port Data.Finset.LocallyFinite (#1837)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Finset/LocallyFinite.lean

added theorem BddAbove.finite

added theorem BddBelow.finite

added theorem BddBelow.finite_of_bddAbove

added theorem Finset.Icc_diff_Ico_self

added theorem Finset.Icc_diff_Ioc_self

added theorem Finset.Icc_diff_Ioo_self

added theorem Finset.Icc_diff_both

added theorem Finset.Icc_eq_cons_Ico

added theorem Finset.Icc_eq_cons_Ioc

added theorem Finset.Icc_eq_empty_iff

added theorem Finset.Icc_eq_empty_of_lt

added theorem Finset.Icc_eq_singleton_iff

added theorem Finset.Icc_erase_left

added theorem Finset.Icc_erase_right

added theorem Finset.Icc_filter_lt_of_lt_right

added theorem Finset.Icc_min_max

added theorem Finset.Icc_sSubset_Icc_left

added theorem Finset.Icc_sSubset_Icc_right

added theorem Finset.Icc_self

added theorem Finset.Icc_subset_Icc

added theorem Finset.Icc_subset_Icc_iff

added theorem Finset.Icc_subset_Icc_left

added theorem Finset.Icc_subset_Icc_right

added theorem Finset.Icc_subset_Ici_self

added theorem Finset.Icc_subset_Ico_iff

added theorem Finset.Icc_subset_Ico_right

added theorem Finset.Icc_subset_Iic_self

added theorem Finset.Icc_subset_Ioc_iff

added theorem Finset.Icc_subset_Ioo_iff

added theorem Finset.Icc_subset_uIcc'

added theorem Finset.Icc_subset_uIcc

added theorem Finset.Ici_eq_cons_Ioi

added theorem Finset.Ici_erase

added theorem Finset.Ico_diff_Ico_left

added theorem Finset.Ico_diff_Ico_right

added theorem Finset.Ico_diff_Ioo_self

added theorem Finset.Ico_disjoint_Ico_consecutive

added theorem Finset.Ico_eq_empty_iff

added theorem Finset.Ico_eq_empty_of_le

added theorem Finset.Ico_erase_left

added theorem Finset.Ico_filter_le

added theorem Finset.Ico_filter_le_left

added theorem Finset.Ico_filter_le_of_le_left

added theorem Finset.Ico_filter_le_of_left_le

added theorem Finset.Ico_filter_le_of_right_le

added theorem Finset.Ico_filter_lt

added theorem Finset.Ico_filter_lt_of_le_left

added theorem Finset.Ico_filter_lt_of_le_right

added theorem Finset.Ico_filter_lt_of_right_le

added theorem Finset.Ico_insert_right

added theorem Finset.Ico_inter_Ico

added theorem Finset.Ico_inter_Ico_consecutive

added theorem Finset.Ico_self

added theorem Finset.Ico_subset_Icc_self

added theorem Finset.Ico_subset_Ici_self

added theorem Finset.Ico_subset_Ico

added theorem Finset.Ico_subset_Ico_iff

added theorem Finset.Ico_subset_Ico_left

added theorem Finset.Ico_subset_Ico_right

added theorem Finset.Ico_subset_Ico_union_Ico

added theorem Finset.Ico_subset_Iic_self

added theorem Finset.Ico_subset_Iio_self

added theorem Finset.Ico_subset_Ioo_left

added theorem Finset.Ico_union_Ico'

added theorem Finset.Ico_union_Ico

added theorem Finset.Ico_union_Ico_eq_Ico

added theorem Finset.Iic_eq_cons_Iio

added theorem Finset.Iic_erase

added theorem Finset.Iic_filter_lt_of_lt_right

added theorem Finset.Iio_filter_lt

added theorem Finset.Iio_insert

added theorem Finset.Iio_subset_Iic_self

added theorem Finset.Ioc_diff_Ioo_self

added theorem Finset.Ioc_eq_empty_iff

added theorem Finset.Ioc_eq_empty_of_le

added theorem Finset.Ioc_erase_right

added theorem Finset.Ioc_filter_lt_of_lt_right

added theorem Finset.Ioc_insert_left

added theorem Finset.Ioc_self

added theorem Finset.Ioc_subset_Icc_self

added theorem Finset.Ioc_subset_Ici_self

added theorem Finset.Ioc_subset_Iic_self

added theorem Finset.Ioc_subset_Ioc

added theorem Finset.Ioc_subset_Ioc_left

added theorem Finset.Ioc_subset_Ioc_right

added theorem Finset.Ioc_subset_Ioi_self

added theorem Finset.Ioc_subset_Ioo_right

added theorem Finset.Ioc_union_Ioc_eq_Ioc

added theorem Finset.Ioi_disjUnion_Iio

added theorem Finset.Ioi_insert

added theorem Finset.Ioi_subset_Ici_self

added theorem Finset.Ioo_eq_empty

added theorem Finset.Ioo_eq_empty_iff

added theorem Finset.Ioo_eq_empty_of_le

added theorem Finset.Ioo_filter_lt

added theorem Finset.Ioo_insert_left

added theorem Finset.Ioo_insert_right

added theorem Finset.Ioo_self

added theorem Finset.Ioo_subset_Icc_self

added theorem Finset.Ioo_subset_Ici_self

added theorem Finset.Ioo_subset_Ico_self

added theorem Finset.Ioo_subset_Iic_self

added theorem Finset.Ioo_subset_Iio_self

added theorem Finset.Ioo_subset_Ioc_self

added theorem Finset.Ioo_subset_Ioi_self

added theorem Finset.Ioo_subset_Ioo

added theorem Finset.Ioo_subset_Ioo_left

added theorem Finset.Ioo_subset_Ioo_right

added theorem Finset.card_Ico_eq_card_Icc_sub_one

added theorem Finset.card_Iio_eq_card_Iic_sub_one

added theorem Finset.card_Ioc_eq_card_Icc_sub_one

added theorem Finset.card_Ioi_eq_card_Ici_sub_one

added theorem Finset.card_Ioo_eq_card_Icc_sub_two

added theorem Finset.card_Ioo_eq_card_Ico_sub_one

added theorem Finset.card_Ioo_eq_card_Ioc_sub_one

added theorem Finset.disjoint_Ioi_Iio

added theorem Finset.eq_of_mem_uIcc_of_mem_uIcc'

added theorem Finset.eq_of_mem_uIcc_of_mem_uIcc

added theorem Finset.filter_ge_eq_Iic

added theorem Finset.filter_gt_eq_Iio

added theorem Finset.filter_le_eq_Ici

added theorem Finset.filter_le_le_eq_Icc

added theorem Finset.filter_le_lt_eq_Ico

added theorem Finset.filter_lt_eq_Ioi

added theorem Finset.filter_lt_le_eq_Ioc

added theorem Finset.filter_lt_lt_eq_Ioo

added theorem Finset.image_add_left_Icc

added theorem Finset.image_add_left_Ico

added theorem Finset.image_add_left_Ioc

added theorem Finset.image_add_left_Ioo

added theorem Finset.image_add_right_Icc

added theorem Finset.image_add_right_Ico

added theorem Finset.image_add_right_Ioc

added theorem Finset.image_add_right_Ioo

added theorem Finset.left_mem_Icc

added theorem Finset.left_mem_Ico

added theorem Finset.left_mem_uIcc

added theorem Finset.left_not_mem_Ioc

added theorem Finset.left_not_mem_Ioo

added theorem Finset.map_add_left_Icc

added theorem Finset.map_add_left_Ico

added theorem Finset.map_add_left_Ioc

added theorem Finset.map_add_left_Ioo

added theorem Finset.map_add_right_Icc

added theorem Finset.map_add_right_Ico

added theorem Finset.map_add_right_Ioc

added theorem Finset.map_add_right_Ioo

added theorem Finset.mem_uIcc'

added theorem Finset.mem_uIcc_of_ge

added theorem Finset.mem_uIcc_of_le

added theorem Finset.nonempty_Icc

added theorem Finset.nonempty_Ico

added theorem Finset.nonempty_Ioc

added theorem Finset.nonempty_Ioo

added theorem Finset.nonempty_uIcc

added theorem Finset.not_mem_Iio_self

added theorem Finset.not_mem_Ioi_self

added theorem Finset.not_mem_uIcc_of_gt

added theorem Finset.not_mem_uIcc_of_lt

added theorem Finset.prod_prod_Ioi_mul_eq_prod_prod_off_diag

added theorem Finset.right_mem_Icc

added theorem Finset.right_mem_Ioc

added theorem Finset.right_mem_uIcc

added theorem Finset.right_not_mem_Ico

added theorem Finset.right_not_mem_Ioo

added theorem Finset.uIcc_comm

added theorem Finset.uIcc_eq_union

added theorem Finset.uIcc_injective_left

added theorem Finset.uIcc_injective_right

added theorem Finset.uIcc_of_ge

added theorem Finset.uIcc_of_le

added theorem Finset.uIcc_of_not_ge

added theorem Finset.uIcc_of_not_le

added theorem Finset.uIcc_self

added theorem Finset.uIcc_subset_Icc

added theorem Finset.uIcc_subset_uIcc

added theorem Finset.uIcc_subset_uIcc_iff_le'

added theorem Finset.uIcc_subset_uIcc_iff_le

added theorem Finset.uIcc_subset_uIcc_iff_mem

added theorem Finset.uIcc_subset_uIcc_left

added theorem Finset.uIcc_subset_uIcc_right

added theorem Finset.uIcc_subset_uIcc_union_uIcc

added theorem Finset.uIcc_toDual

added def Set.fintypeOfMemBounds

Modified Mathlib/Data/Set/Intervals/OrdConnected.lean

Modified Mathlib/Data/Set/Intervals/OrdConnectedComponent.lean

Modified Mathlib/Data/Set/Intervals/UnorderedInterval.lean

Modified Mathlib/Order/Filter/Interval.lean