Documentation Verification Report

Order

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

Statistics

Metric	Count
Definitions `boundedOrder`, `le`, `linearOrder`, `lt`, `orderBot`, `orderTop`, `partialOrder`, `preorder`, `«termΣₗ'_,_»`	9
Theorems `denselyOrdered`, `denselyOrdered_of_noMaxOrder`, `denselyOrdered_of_noMinOrder`, `noMaxOrder`, `noMaxOrder_of_nonempty`, `noMinOrder`, `noMinOrder_of_nonempty`	7
Total	16

PSigma

Definitions

Name	Category	Theorems
`«termΣₗ'_,_»` 📖	CompOp	—

PSigma.Lex

Definitions

Name	Category	Theorems
`boundedOrder` 📖	CompOp	—
`le` 📖	CompOp	—
`linearOrder` 📖	CompOp	—
`lt` 📖	CompOp	7 math math: `denselyOrdered_of_noMinOrder`, `noMaxOrder_of_nonempty`, `noMinOrder`, `noMaxOrder`, `noMinOrder_of_nonempty`, `denselyOrdered`, `denselyOrdered_of_noMaxOrder`
`orderBot` 📖	CompOp	—
`orderTop` 📖	CompOp	—
`partialOrder` 📖	CompOp	—
`preorder` 📖	CompOp	—

Theorems

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

---

← Back to Index