Documentation Verification Report

Interval

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

Statistics

Metric	Count
Definitions `instLocallyFiniteOrder`	1
Theorems `Icc_eq`, `card_Icc`, `card_Ico`, `card_Iic`, `card_Ioc`, `card_Ioo`, `card_uIcc`, `uIcc_eq`	8
Total	9

Multiset

Definitions

Name	Category	Theorems
`instLocallyFiniteOrder` 📖	CompOp	8 math math: `card_Ico`, `Icc_eq`, `card_Ioc`, `card_uIcc`, `uIcc_eq`, `card_Iic`, `card_Icc`, `card_Ioo`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`Icc_eq` 📖	mathematical	—	`Finset.Icc` `Multiset` `PartialOrder.toPreorder` `instPartialOrder` `instLocallyFiniteOrder` `Finset.map` `DFinsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Equiv.toEmbedding` `Equiv.symm` `AddEquiv.toEquiv` `instAdd` `DFinsupp.instAdd` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `equivDFinsupp` `DFinsupp.instPreorder` `Nat.instPreorder` `DFinsupp.instLocallyFiniteOrder` `Nat.instPartialOrder` `Nat.instLocallyFiniteOrder` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddCommMonoid.toAddMonoid` `AddCancelCommMonoid.toAddCommMonoid` `instAddCancelCommMonoid` `DFinsupp.addZeroClass'` `AddMonoidHom.instFunLike` `toDFinsupp`	—	—
`card_Icc` 📖	mathematical	—	`Finset.card` `Multiset` `Finset.Icc` `PartialOrder.toPreorder` `instPartialOrder` `instLocallyFiniteOrder` `Finset.prod` `Nat.instCommMonoid` `Finset` `Finset.instUnion` `toFinset` `count`	—	`Finset.card_map` `DFinsupp.card_Icc` `Finset.prod_congr` `Nat.card_Icc` `toDFinsupp_support`
`card_Ico` 📖	mathematical	—	`Finset.card` `Multiset` `Finset.Ico` `PartialOrder.toPreorder` `instPartialOrder` `instLocallyFiniteOrder` `Finset.prod` `Nat.instCommMonoid` `Finset` `Finset.instUnion` `toFinset` `count`	—	`Finset.card_Ico_eq_card_Icc_sub_one` `card_Icc`
`card_Iic` 📖	mathematical	—	`Finset.card` `Multiset` `Finset.Iic` `PartialOrder.toPreorder` `instPartialOrder` `LocallyFiniteOrder.toLocallyFiniteOrderBot` `instOrderBot` `instLocallyFiniteOrder` `Finset.prod` `Nat.instCommMonoid` `toFinset` `count`	—	`card_Icc` `Finset.prod_congr` `Finset.empty_union` `tsub_zero` `Nat.instOrderedSub`
`card_Ioc` 📖	mathematical	—	`Finset.card` `Multiset` `Finset.Ioc` `PartialOrder.toPreorder` `instPartialOrder` `instLocallyFiniteOrder` `Finset.prod` `Nat.instCommMonoid` `Finset` `Finset.instUnion` `toFinset` `count`	—	`Finset.card_Ioc_eq_card_Icc_sub_one` `card_Icc`
`card_Ioo` 📖	mathematical	—	`Finset.card` `Multiset` `Finset.Ioo` `PartialOrder.toPreorder` `instPartialOrder` `instLocallyFiniteOrder` `Finset.prod` `Nat.instCommMonoid` `Finset` `Finset.instUnion` `toFinset` `count`	—	`Finset.card_Ioo_eq_card_Icc_sub_two` `card_Icc`
`card_uIcc` 📖	mathematical	—	`Finset.card` `Multiset` `Finset.uIcc` `instLattice` `instLocallyFiniteOrder` `Finset.prod` `Nat.instCommMonoid` `Finset` `Finset.instUnion` `toFinset` `count`	—	`uIcc_eq` `Finset.card_map` `DFinsupp.card_uIcc` `Finset.prod_congr` `Nat.card_uIcc` `toDFinsupp_support`
`uIcc_eq` 📖	mathematical	—	`Finset.uIcc` `Multiset` `instLattice` `instLocallyFiniteOrder` `Finset.map` `DFinsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Equiv.toEmbedding` `Equiv.symm` `AddEquiv.toEquiv` `instAdd` `DFinsupp.instAdd` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `equivDFinsupp` `DFinsupp.lattice` `Nat.instLattice` `DFinsupp.instLocallyFiniteOrder` `Nat.instPartialOrder` `Nat.instLocallyFiniteOrder` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddCommMonoid.toAddMonoid` `AddCancelCommMonoid.toAddCommMonoid` `instAddCancelCommMonoid` `DFinsupp.addZeroClass'` `AddMonoidHom.instFunLike` `toDFinsupp`	—	`Icc_eq` `toDFinsupp_inter` `toDFinsupp_union`

---

← Back to Index