Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-01 12:55 0144b6ca

View on Github →

chore({data/finset,data/multiset,order}/locally_finite): Better line wraps (#10087)

Estimated changes

modified theorem finset.Icc_eq_empty_of_lt
modified theorem finset.Icc_self
modified theorem finset.Ico_eq_empty_of_le
modified theorem finset.Ico_self
modified theorem finset.Ioc_eq_empty_of_le
modified theorem finset.Ioc_self
modified theorem finset.Ioo_eq_empty_of_le
modified theorem finset.Ioo_self
modified theorem multiset.Icc_eq_zero_of_lt
modified theorem multiset.Icc_self
modified theorem multiset.Ioc_eq_zero_of_le
modified theorem multiset.Ioc_self
modified theorem multiset.Ioo_eq_zero_of_le
modified theorem multiset.Ioo_self
modified def finset.Icc
modified def finset.Ico
modified theorem finset.Ico_subset_Ico
modified def finset.Iic
modified def finset.Iio
modified def finset.Ioc
modified def finset.Ioo
modified theorem finset.mem_Ici
modified theorem finset.mem_Iic
modified theorem finset.mem_Iio
modified theorem finset.mem_Ioi
modified def multiset.Icc
modified def multiset.Ici
modified def multiset.Iic
modified def multiset.Iio
modified def multiset.Ioc
modified def multiset.Ioi
modified def multiset.Ioo
modified theorem multiset.mem_Ici
modified theorem multiset.mem_Iic
modified theorem multiset.mem_Iio
modified theorem multiset.mem_Ioi
modified theorem set.finite_Ici
modified theorem set.finite_Iic
modified theorem set.finite_Iio
modified theorem set.finite_Ioi