Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-11 13:55 4ac13d92

View on Github →

feat(data/dfinsupp/interval): Finitely supported dependent functions to locally finite orders are locally finite (#11175) This provides the locally_finite_order instance for Π₀ i, α i in a new file data.dfinsupp.interval.

Estimated changes

modified theorem dfinsupp.mem_support_iff
modified theorem dfinsupp.mk_apply
added theorem dfinsupp.mk_of_mem
added theorem dfinsupp.mk_of_not_mem
added theorem dfinsupp.card_Icc
added theorem dfinsupp.card_Ico
added theorem dfinsupp.card_Ioc
added theorem dfinsupp.card_Ioo
added theorem dfinsupp.card_pi
added theorem dfinsupp.mem_pi
added def dfinsupp.pi
added theorem finset.card_dfinsupp
added def finset.dfinsupp
modified theorem dfinsupp.le_iff'
modified theorem dfinsupp.le_iff
modified theorem dfinsupp.single_le_iff
added theorem finset.not_mem_mono
modified theorem multiset.cons_le_cons
modified theorem multiset.cons_le_cons_iff
modified theorem multiset.le_cons_of_not_mem
modified theorem multiset.le_zero
modified theorem multiset.mem_of_le
added theorem multiset.not_mem_mono
modified theorem multiset.subset_of_le