Documentation Verification Report

Order

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

Statistics

Metric	Count
Definitions `LE`, `LT`, `LE`, `LT`, `boundedOrder`, `linearOrder`, `orderBot`, `orderTop`, `partialOrder`, `preorder`, `«termΣₗ_,_»`, `instLE_mathlib`, `instLT_mathlib`, `instPartialOrder`, `preorder`	15
Theorems `denselyOrdered`, `denselyOrdered_of_noMaxOrder`, `denselyOrdered_of_noMinOrder`, `le_def`, `lt_def`, `noMaxOrder`, `noMaxOrder_of_nonempty`, `noMinOrder`, `noMinOrder_of_nonempty`, `instDenselyOrdered`, `le_def`, `lt_def`, `mk_le_mk_iff`, `mk_lt_mk_iff`	14
Total	29

Sigma

Definitions

Name	Category	Theorems
`LE` 📖	CompData	—
`LT` 📖	CompData	—
`instLE_mathlib` 📖	CompOp	2 math math: `le_def`, `mk_le_mk_iff`
`instLT_mathlib` 📖	CompOp	3 math math: `lt_def`, `mk_lt_mk_iff`, `instDenselyOrdered`
`instPartialOrder` 📖	CompOp	—
`preorder` 📖	CompOp	12 math math: `Ici_mk`, `Iic_mk`, `Ico_mk_mk`, `Icc_mk_mk`, `Iio_mk`, `Ioc_mk_mk`, `Ioi_mk`, `card_Ioo`, `card_Ico`, `card_Ioc`, `card_Icc`, `Ioo_mk_mk`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instDenselyOrdered` 📖	mathematical	`DenselyOrdered` `Preorder.toLT`	`instLT_mathlib`	—	`exists_between`
`le_def` 📖	mathematical	—	`instLE_mathlib`	—	—
`lt_def` 📖	mathematical	—	`instLT_mathlib`	—	—
`mk_le_mk_iff` 📖	mathematical	—	`instLE_mathlib`	—	—
`mk_lt_mk_iff` 📖	mathematical	—	`instLT_mathlib`	—	—

Sigma.Lex

Definitions

Name	Category	Theorems
`LE` 📖	CompOp	1 math math: `le_def`
`LT` 📖	CompOp	8 math math: `denselyOrdered_of_noMaxOrder`, `denselyOrdered_of_noMinOrder`, `noMaxOrder_of_nonempty`, `noMinOrder`, `noMaxOrder`, `denselyOrdered`, `lt_def`, `noMinOrder_of_nonempty`
`boundedOrder` 📖	CompOp	—
`linearOrder` 📖	CompOp	—
`orderBot` 📖	CompOp	—
`orderTop` 📖	CompOp	—
`partialOrder` 📖	CompOp	—
`preorder` 📖	CompOp	—
`«termΣₗ_,_»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`denselyOrdered` 📖	mathematical	`DenselyOrdered` `Preorder.toLT`	`Lex` `LT`	—	`exists_between`
`denselyOrdered_of_noMaxOrder` 📖	mathematical	`DenselyOrdered` `Preorder.toLT` `NoMaxOrder`	`Lex` `LT`	—	`NoMaxOrder.exists_gt` `exists_between`
`denselyOrdered_of_noMinOrder` 📖	mathematical	`DenselyOrdered` `Preorder.toLT` `NoMinOrder`	`Lex` `LT`	—	`NoMinOrder.exists_lt` `exists_between`
`le_def` 📖	mathematical	—	`Lex` `LE`	—	`Sigma.lex_iff`
`lt_def` 📖	mathematical	—	`Lex` `LT`	—	`Sigma.lex_iff`
`noMaxOrder` 📖	mathematical	`NoMaxOrder` `Preorder.toLT`	`Lex` `LT`	—	`NoMaxOrder.exists_gt`
`noMaxOrder_of_nonempty` 📖	mathematical	—	`NoMaxOrder` `Lex` `LT` `Preorder.toLT`	—	`NoMaxOrder.exists_gt`
`noMinOrder` 📖	mathematical	`NoMinOrder` `Preorder.toLT`	`Lex` `LT`	—	`NoMinOrder.exists_lt`
`noMinOrder_of_nonempty` 📖	mathematical	—	`NoMinOrder` `Lex` `LT` `Preorder.toLT`	—	`NoMinOrder.exists_lt`

---

← Back to Index