Documentation Verification Report

Interval

📁 Source: Mathlib/Data/DFinsupp/Interval.lean

Statistics

Metric	Count
Definitions `instLocallyFiniteOrder`, `pi`, `rangeIcc`, `singleton`, `dfinsupp`	5
Theorems `Icc_eq`, `card_Icc`, `card_Ico`, `card_Iic`, `card_Iio`, `card_Ioc`, `card_Ioo`, `card_pi`, `card_uIcc`, `mem_pi`, `mem_rangeIcc_apply_iff`, `mem_singleton_apply_iff`, `rangeIcc_apply`, `support_rangeIcc_subset`, `card_dfinsupp`, `mem_dfinsupp_iff`, `mem_dfinsupp_iff_of_support_subset`	17
Total	22

DFinsupp

Definitions

Name	Category	Theorems
`instLocallyFiniteOrder` 📖	CompOp	10 math math: `Multiset.Icc_eq`, `card_Iic`, `card_Ioo`, `Multiset.uIcc_eq`, `Icc_eq`, `card_uIcc`, `card_Ico`, `card_Iio`, `card_Icc`, `card_Ioc`
`pi` 📖	CompOp	2 math math: `card_pi`, `mem_pi`
`rangeIcc` 📖	CompOp	4 math math: `support_rangeIcc_subset`, `Icc_eq`, `rangeIcc_apply`, `mem_rangeIcc_apply_iff`
`singleton` 📖	CompOp	1 math math: `mem_singleton_apply_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`Icc_eq` 📖	mathematical	—	`Finset.Icc` `DFinsupp` `instPreorder` `PartialOrder.toPreorder` `instLocallyFiniteOrder` `Finset.dfinsupp` `Finset` `Finset.instUnion` `support` `DFunLike.coe` `Finset.zero` `instDFunLike` `rangeIcc`	—	—
`card_Icc` 📖	mathematical	—	`Finset.card` `DFinsupp` `Finset.Icc` `instPreorder` `PartialOrder.toPreorder` `instLocallyFiniteOrder` `Finset.prod` `Nat.instCommMonoid` `Finset` `Finset.instUnion` `support` `DFunLike.coe` `instDFunLike`	—	`Finset.card_dfinsupp`
`card_Ico` 📖	mathematical	—	`Finset.card` `DFinsupp` `Finset.Ico` `instPreorder` `PartialOrder.toPreorder` `instLocallyFiniteOrder` `Finset.prod` `Nat.instCommMonoid` `Finset` `Finset.instUnion` `support` `Finset.Icc` `DFunLike.coe` `instDFunLike`	—	`Finset.card_Ico_eq_card_Icc_sub_one` `card_Icc`
`card_Iic` 📖	mathematical	`CanonicallyOrderedAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `Preorder.toLE` `PartialOrder.toPreorder`	`Finset.card` `DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Finset.Iic` `instPreorder` `LocallyFiniteOrder.toLocallyFiniteOrderBot` `instOrderBot` `instLocallyFiniteOrder` `Finset.prod` `Nat.instCommMonoid` `support` `DFunLike.coe` `instDFunLike`	—	`Finset.prod_congr` `card_Icc` `Finset.empty_union` `bot_eq_zero`
`card_Iio` 📖	mathematical	`CanonicallyOrderedAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `Preorder.toLE` `PartialOrder.toPreorder`	`Finset.card` `DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Finset.Iio` `instPreorder` `LocallyFiniteOrder.toLocallyFiniteOrderBot` `instOrderBot` `instLocallyFiniteOrder` `Finset.prod` `Nat.instCommMonoid` `support` `Finset.Iic` `DFunLike.coe` `instDFunLike`	—	`Finset.card_Iio_eq_card_Iic_sub_one` `card_Iic`
`card_Ioc` 📖	mathematical	—	`Finset.card` `DFinsupp` `Finset.Ioc` `instPreorder` `PartialOrder.toPreorder` `instLocallyFiniteOrder` `Finset.prod` `Nat.instCommMonoid` `Finset` `Finset.instUnion` `support` `Finset.Icc` `DFunLike.coe` `instDFunLike`	—	`Finset.card_Ioc_eq_card_Icc_sub_one` `card_Icc`
`card_Ioo` 📖	mathematical	—	`Finset.card` `DFinsupp` `Finset.Ioo` `instPreorder` `PartialOrder.toPreorder` `instLocallyFiniteOrder` `Finset.prod` `Nat.instCommMonoid` `Finset` `Finset.instUnion` `support` `Finset.Icc` `DFunLike.coe` `instDFunLike`	—	`Finset.card_Ioo_eq_card_Icc_sub_two` `card_Icc`
`card_pi` 📖	mathematical	—	`Finset.card` `DFinsupp` `pi` `prod` `Finset` `Finset.zero` `Finset.decidableEq` `Nat.instCommMonoid` `Pi.instNatCast` `DFunLike.coe` `instDFunLike`	—	`pi.eq_1` `Finset.card_dfinsupp` `Finset.prod_congr`
`card_uIcc` 📖	mathematical	—	`Finset.card` `DFinsupp` `Finset.uIcc` `lattice` `instLocallyFiniteOrder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `Finset.prod` `Nat.instCommMonoid` `Finset` `Finset.instUnion` `support` `DFunLike.coe` `instDFunLike`	—	`support_inf_union_support_sup` `card_Icc`
`mem_pi` 📖	mathematical	—	`DFinsupp` `Finset` `Finset.instMembership` `pi` `DFunLike.coe` `Finset.zero` `instDFunLike`	—	`Finset.mem_dfinsupp_iff_of_support_subset` `Finset.Subset.refl`
`mem_rangeIcc_apply_iff` 📖	mathematical	—	`Finset` `Finset.instMembership` `DFunLike.coe` `DFinsupp` `Finset.zero` `instDFunLike` `rangeIcc` `Preorder.toLE` `PartialOrder.toPreorder`	—	`Finset.mem_Icc`
`mem_singleton_apply_iff` 📖	mathematical	—	`Finset` `Finset.instMembership` `DFunLike.coe` `DFinsupp` `Finset.zero` `instDFunLike` `singleton`	—	`Finset.mem_singleton`
`rangeIcc_apply` 📖	mathematical	—	`DFunLike.coe` `DFinsupp` `Finset` `Finset.zero` `instDFunLike` `rangeIcc` `Finset.Icc` `PartialOrder.toPreorder`	—	—
`support_rangeIcc_subset` 📖	mathematical	—	`Finset` `Finset.instHasSubset` `support` `Finset.zero` `Finset.decidableEq` `rangeIcc` `Finset.instUnion`	—	`notMem_support_iff` `rangeIcc_apply` `Finset.notMem_mono` `Finset.subset_union_left` `Finset.subset_union_right` `Finset.Icc_self`

Finset

Definitions

Name	Category	Theorems
`dfinsupp` 📖	CompOp	4 math math: `mem_dfinsupp_iff_of_support_subset`, `card_dfinsupp`, `DFinsupp.Icc_eq`, `mem_dfinsupp_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_dfinsupp` 📖	mathematical	—	`card` `DFinsupp` `dfinsupp` `prod` `Nat.instCommMonoid`	—	`card_map` `card_pi`
`mem_dfinsupp_iff` 📖	mathematical	—	`DFinsupp` `Finset` `instMembership` `dfinsupp` `instHasSubset` `DFinsupp.support` `DFunLike.coe` `DFinsupp.instDFunLike`	—	`mem_map` `DFinsupp.support_mk_subset` `DFinsupp.mk_of_mem` `mem_pi` `DFinsupp.ext` `DFinsupp.notMem_support_iff`
`mem_dfinsupp_iff_of_support_subset` 📖	mathematical	`Finset` `instHasSubset` `DFinsupp.support` `zero` `decidableEq`	`DFinsupp` `instMembership` `dfinsupp` `DFunLike.coe` `DFinsupp.instDFunLike`	—	`mem_dfinsupp_iff` `DFinsupp.notMem_support_iff` `notMem_mono` `zero_mem_zero` `DFinsupp.mem_support_iff` `mem_zero`

---

← Back to Index