Documentation Verification Report

Interval

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

Statistics

Metric	Count
Definitions `instLocallyFiniteOrder`, `rangeIcc`, `rangeSingleton`	3
Theorems `Icc_eq`, `card_Icc`, `card_Ico`, `card_Iic`, `card_Iio`, `card_Ioc`, `card_Ioo`, `card_uIcc`, `coe_rangeIcc`, `mem_rangeIcc_apply_iff`, `mem_rangeSingleton_apply_iff`, `rangeIcc_apply`, `rangeIcc_support`, `rangeIcc_toFun`, `rangeSingleton_apply`, `rangeSingleton_support`	16
Total	19

Finsupp

Definitions

Name	Category	Theorems
`instLocallyFiniteOrder` 📖	CompOp	8 math math: `card_Ioc`, `card_Ico`, `card_Icc`, `card_uIcc`, `card_Ioo`, `card_Iic`, `card_Iio`, `Icc_eq`
`rangeIcc` 📖	CompOp	6 math math: `rangeIcc_toFun`, `rangeIcc_apply`, `mem_rangeIcc_apply_iff`, `coe_rangeIcc`, `Icc_eq`, `rangeIcc_support`
`rangeSingleton` 📖	CompOp	3 math math: `rangeSingleton_support`, `mem_rangeSingleton_apply_iff`, `rangeSingleton_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`Icc_eq` 📖	mathematical	—	`Finset.Icc` `Finsupp` `preorder` `PartialOrder.toPreorder` `instLocallyFiniteOrder` `Finset.finsupp` `Finset` `Finset.instUnion` `support` `DFunLike.coe` `Finset.zero` `instFunLike` `rangeIcc`	—	—
`card_Icc` 📖	mathematical	—	`Finset.card` `Finsupp` `Finset.Icc` `preorder` `PartialOrder.toPreorder` `instLocallyFiniteOrder` `Finset.prod` `Nat.instCommMonoid` `Finset` `Finset.instUnion` `support` `DFunLike.coe` `instFunLike`	—	`Finset.card_finsupp` `Finset.prod_congr`
`card_Ico` 📖	mathematical	—	`Finset.card` `Finsupp` `Finset.Ico` `preorder` `PartialOrder.toPreorder` `instLocallyFiniteOrder` `Finset.prod` `Nat.instCommMonoid` `Finset` `Finset.instUnion` `support` `Finset.Icc` `DFunLike.coe` `instFunLike`	—	`Finset.card_Ico_eq_card_Icc_sub_one` `card_Icc`
`card_Iic` 📖	mathematical	—	`Finset.card` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Finset.Iic` `preorder` `PartialOrder.toPreorder` `LocallyFiniteOrder.toLocallyFiniteOrderBot` `orderBot` `instLocallyFiniteOrder` `Finset.prod` `Nat.instCommMonoid` `support` `DFunLike.coe` `instFunLike`	—	`Finset.prod_congr` `card_Icc` `Finset.empty_union` `bot_eq_zero`
`card_Iio` 📖	mathematical	—	`Finset.card` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Finset.Iio` `preorder` `PartialOrder.toPreorder` `LocallyFiniteOrder.toLocallyFiniteOrderBot` `orderBot` `instLocallyFiniteOrder` `Finset.prod` `Nat.instCommMonoid` `support` `Finset.Iic` `DFunLike.coe` `instFunLike`	—	`Finset.card_Iio_eq_card_Iic_sub_one` `card_Iic`
`card_Ioc` 📖	mathematical	—	`Finset.card` `Finsupp` `Finset.Ioc` `preorder` `PartialOrder.toPreorder` `instLocallyFiniteOrder` `Finset.prod` `Nat.instCommMonoid` `Finset` `Finset.instUnion` `support` `Finset.Icc` `DFunLike.coe` `instFunLike`	—	`Finset.card_Ioc_eq_card_Icc_sub_one` `card_Icc`
`card_Ioo` 📖	mathematical	—	`Finset.card` `Finsupp` `Finset.Ioo` `preorder` `PartialOrder.toPreorder` `instLocallyFiniteOrder` `Finset.prod` `Nat.instCommMonoid` `Finset` `Finset.instUnion` `support` `Finset.Icc` `DFunLike.coe` `instFunLike`	—	`Finset.card_Ioo_eq_card_Icc_sub_two` `card_Icc`
`card_uIcc` 📖	mathematical	—	`Finset.card` `Finsupp` `Finset.uIcc` `lattice` `instLocallyFiniteOrder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `Finset.prod` `Nat.instCommMonoid` `Finset` `Finset.instUnion` `support` `DFunLike.coe` `instFunLike`	—	`support_inf_union_support_sup` `card_Icc`
`coe_rangeIcc` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `Finset` `Finset.zero` `instFunLike` `rangeIcc` `Finset.Icc` `PartialOrder.toPreorder`	—	—
`mem_rangeIcc_apply_iff` 📖	mathematical	—	`Finset` `Finset.instMembership` `DFunLike.coe` `Finsupp` `Finset.zero` `instFunLike` `rangeIcc` `Preorder.toLE` `PartialOrder.toPreorder`	—	`Finset.mem_Icc`
`mem_rangeSingleton_apply_iff` 📖	mathematical	—	`Finset` `Finset.instMembership` `DFunLike.coe` `Finsupp` `Finset.zero` `instFunLike` `rangeSingleton`	—	`Finset.mem_singleton`
`rangeIcc_apply` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `Finset` `Finset.zero` `instFunLike` `rangeIcc` `Finset.Icc` `PartialOrder.toPreorder`	—	—
`rangeIcc_support` 📖	mathematical	—	`support` `Finset` `Finset.zero` `rangeIcc` `Finset.instUnion`	—	—
`rangeIcc_toFun` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `Finset` `Finset.zero` `instFunLike` `rangeIcc` `Finset.Icc` `PartialOrder.toPreorder`	—	`rangeIcc_apply`
`rangeSingleton_apply` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `Finset` `Finset.zero` `instFunLike` `rangeSingleton` `Finset.instSingleton`	—	—
`rangeSingleton_support` 📖	mathematical	—	`support` `Finset` `Finset.zero` `rangeSingleton`	—	—

---

← Back to Index