Documentation Verification Report

Interval

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

Statistics

Metric	Count
Definitions `instLocallyFiniteOrder`, `instLocallyFiniteOrderBot`, `instLocallyFiniteOrderTop`	3
Theorems `Icc_eq`, `card_Icc`, `card_Ici`, `card_Ico`, `card_Iic`, `card_Iio`, `card_Ioc`, `card_Ioi`, `card_Ioo`, `card_uIcc`, `uIcc_eq`	11
Total	14

Pi

Definitions

Name	Category	Theorems
`instLocallyFiniteOrder` 📖	CompOp	7 math math: `card_Ioc`, `card_Icc`, `card_uIcc`, `uIcc_eq`, `card_Ico`, `card_Ioo`, `Icc_eq`
`instLocallyFiniteOrderBot` 📖	CompOp	2 math math: `card_Iic`, `card_Iio`
`instLocallyFiniteOrderTop` 📖	CompOp	2 math math: `card_Ici`, `card_Ioi`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`Icc_eq` 📖	mathematical	—	`Finset.Icc` `preorder` `PartialOrder.toPreorder` `instLocallyFiniteOrder` `Fintype.piFinset`	—	—
`card_Icc` 📖	mathematical	—	`Finset.card` `Finset.Icc` `preorder` `PartialOrder.toPreorder` `instLocallyFiniteOrder` `Finset.prod` `Nat.instCommMonoid` `Finset.univ`	—	`Fintype.card_piFinset`
`card_Ici` 📖	mathematical	—	`Finset.card` `Finset.Ici` `preorder` `PartialOrder.toPreorder` `instLocallyFiniteOrderTop` `Finset.prod` `Nat.instCommMonoid` `Finset.univ`	—	`Fintype.card_piFinset`
`card_Ico` 📖	mathematical	—	`Finset.card` `Finset.Ico` `preorder` `PartialOrder.toPreorder` `instLocallyFiniteOrder` `Finset.prod` `Nat.instCommMonoid` `Finset.univ` `Finset.Icc`	—	`Finset.card_Ico_eq_card_Icc_sub_one` `card_Icc`
`card_Iic` 📖	mathematical	—	`Finset.card` `Finset.Iic` `preorder` `PartialOrder.toPreorder` `instLocallyFiniteOrderBot` `Finset.prod` `Nat.instCommMonoid` `Finset.univ`	—	`Fintype.card_piFinset`
`card_Iio` 📖	mathematical	—	`Finset.card` `Finset.Iio` `preorder` `PartialOrder.toPreorder` `instLocallyFiniteOrderBot` `Finset.prod` `Nat.instCommMonoid` `Finset.univ` `Finset.Iic`	—	`Finset.card_Iio_eq_card_Iic_sub_one` `card_Iic`
`card_Ioc` 📖	mathematical	—	`Finset.card` `Finset.Ioc` `preorder` `PartialOrder.toPreorder` `instLocallyFiniteOrder` `Finset.prod` `Nat.instCommMonoid` `Finset.univ` `Finset.Icc`	—	`Finset.card_Ioc_eq_card_Icc_sub_one` `card_Icc`
`card_Ioi` 📖	mathematical	—	`Finset.card` `Finset.Ioi` `preorder` `PartialOrder.toPreorder` `instLocallyFiniteOrderTop` `Finset.prod` `Nat.instCommMonoid` `Finset.univ` `Finset.Ici`	—	`Finset.card_Ioi_eq_card_Ici_sub_one` `card_Ici`
`card_Ioo` 📖	mathematical	—	`Finset.card` `Finset.Ioo` `preorder` `PartialOrder.toPreorder` `instLocallyFiniteOrder` `Finset.prod` `Nat.instCommMonoid` `Finset.univ` `Finset.Icc`	—	`Finset.card_Ioo_eq_card_Icc_sub_two` `card_Icc`
`card_uIcc` 📖	mathematical	—	`Finset.card` `Finset.uIcc` `instLattice` `instLocallyFiniteOrder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `Finset.prod` `Nat.instCommMonoid` `Finset.univ`	—	`card_Icc`
`uIcc_eq` 📖	mathematical	—	`Finset.uIcc` `instLattice` `instLocallyFiniteOrder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `Fintype.piFinset`	—	—

---

← Back to Index