Documentation Verification Report

Interval

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

Statistics

Metric	Count
Definitions `instLocallyFiniteOrder`, `instLocallyFiniteOrderBot`, `instLocallyFiniteOrderTop`	3
Theorems `Icc_mk_mk`, `Ici_mk`, `Ico_mk_mk`, `Iic_mk`, `Iio_mk`, `Ioc_mk_mk`, `Ioi_mk`, `Ioo_mk_mk`, `card_Icc`, `card_Ico`, `card_Ioc`, `card_Ioo`	12
Total	15

Sigma

Definitions

Name	Category	Theorems
`instLocallyFiniteOrder` 📖	CompOp	8 math math: `Ico_mk_mk`, `Icc_mk_mk`, `Ioc_mk_mk`, `card_Ioo`, `card_Ico`, `card_Ioc`, `card_Icc`, `Ioo_mk_mk`
`instLocallyFiniteOrderBot` 📖	CompOp	2 math math: `Iic_mk`, `Iio_mk`
`instLocallyFiniteOrderTop` 📖	CompOp	2 math math: `Ici_mk`, `Ioi_mk`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`Icc_mk_mk` 📖	mathematical	—	`Finset.Icc` `preorder` `instLocallyFiniteOrder` `Finset.map` `Function.Embedding.sigmaMk`	—	—
`Ici_mk` 📖	mathematical	—	`Finset.Ici` `preorder` `instLocallyFiniteOrderTop` `Finset.map` `Function.Embedding.sigmaMk`	—	—
`Ico_mk_mk` 📖	mathematical	—	`Finset.Ico` `preorder` `instLocallyFiniteOrder` `Finset.map` `Function.Embedding.sigmaMk`	—	—
`Iic_mk` 📖	mathematical	—	`Finset.Iic` `preorder` `instLocallyFiniteOrderBot` `Finset.map` `Function.Embedding.sigmaMk`	—	—
`Iio_mk` 📖	mathematical	—	`Finset.Iio` `preorder` `instLocallyFiniteOrderBot` `Finset.map` `Function.Embedding.sigmaMk`	—	—
`Ioc_mk_mk` 📖	mathematical	—	`Finset.Ioc` `preorder` `instLocallyFiniteOrder` `Finset.map` `Function.Embedding.sigmaMk`	—	—
`Ioi_mk` 📖	mathematical	—	`Finset.Ioi` `preorder` `instLocallyFiniteOrderTop` `Finset.map` `Function.Embedding.sigmaMk`	—	—
`Ioo_mk_mk` 📖	mathematical	—	`Finset.Ioo` `preorder` `instLocallyFiniteOrder` `Finset.map` `Function.Embedding.sigmaMk`	—	—
`card_Icc` 📖	mathematical	—	`Finset.card` `Finset.Icc` `preorder` `instLocallyFiniteOrder`	—	`Finset.card_sigmaLift`
`card_Ico` 📖	mathematical	—	`Finset.card` `Finset.Ico` `preorder` `instLocallyFiniteOrder`	—	`Finset.card_sigmaLift`
`card_Ioc` 📖	mathematical	—	`Finset.card` `Finset.Ioc` `preorder` `instLocallyFiniteOrder`	—	`Finset.card_sigmaLift`
`card_Ioo` 📖	mathematical	—	`Finset.card` `Finset.Ioo` `preorder` `instLocallyFiniteOrder`	—	`Finset.card_sigmaLift`

---

← Back to Index