Commit 2023-01-26 10:33 ad4c81eb

View on Github →

feat: port Data.Nat.Interval (#1838)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Nat/Interval.lean

added theorem Finset.range_add_eq_union

added theorem Finset.range_eq_Ico

added theorem Finset.range_image_pred_top_sub

added theorem Nat.Icc_eq_range'

added theorem Nat.Icc_pred_right

added theorem Nat.Icc_succ_left

added theorem Nat.Ico_eq_range'

added theorem Nat.Ico_image_const_sub_eq_Ico

added theorem Nat.Ico_insert_succ_left

added theorem Nat.Ico_pred_singleton

added theorem Nat.Ico_succ_left

added theorem Nat.Ico_succ_left_eq_erase_Ico

added theorem Nat.Ico_succ_right

added theorem Nat.Ico_succ_right_eq_insert_Ico

added theorem Nat.Ico_succ_singleton

added theorem Nat.Ico_succ_succ

added theorem Nat.Ico_zero_eq_range

added theorem Nat.Iio_eq_range

added theorem Nat.Ioc_eq_range'

added theorem Nat.Ioc_succ_singleton

added theorem Nat.Ioo_eq_range'

added theorem Nat.card_Icc

added theorem Nat.card_Ico

added theorem Nat.card_Iic

added theorem Nat.card_Iio

added theorem Nat.card_Ioc

added theorem Nat.card_Ioo

added theorem Nat.card_fintypeIcc

added theorem Nat.card_fintypeIco

added theorem Nat.card_fintypeIic

added theorem Nat.card_fintypeIio

added theorem Nat.card_fintypeIoc

added theorem Nat.card_fintypeIoo

added theorem Nat.cauchy_induction'

added theorem Nat.cauchy_induction

added theorem Nat.cauchy_induction_mul

added theorem Nat.cauchy_induction_two_mul

added theorem Nat.decreasing_induction_of_infinite

added theorem Nat.decreasing_induction_of_not_bddAbove

added theorem Nat.image_Ico_mod

added theorem Nat.image_sub_const_Ico

added theorem Nat.mod_injOn_Ico

added theorem Nat.multiset_Ico_map_mod