Documentation Verification Report

Lex

📁 Source: Mathlib/Order/Interval/Lex.lean

Statistics

Metric	Count
Definitions `instDecidableLELexOfDecidableEqOfDecidableLT`, `instDecidableLTLexOfDecidableEq`, `instLELex`, `instLTLex`, `instLinearOrderLex`, `instPartialOrderLex`, `instPreorderLex`	7
Theorems `toLex_le_toLex`, `toLex_lt_toLex`, `toLex_mono`, `toLex_strictMono`	4
Total	11

NonemptyInterval

Definitions

Name	Category	Theorems
`instDecidableLELexOfDecidableEqOfDecidableLT` 📖	CompOp	—
`instDecidableLTLexOfDecidableEq` 📖	CompOp	—
`instLELex` 📖	CompOp	1 math math: `toLex_le_toLex`
`instLTLex` 📖	CompOp	1 math math: `toLex_lt_toLex`
`instLinearOrderLex` 📖	CompOp	—
`instPartialOrderLex` 📖	CompOp	—
`instPreorderLex` 📖	CompOp	2 math math: `toLex_strictMono`, `toLex_mono`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toLex_le_toLex` 📖	mathematical	—	`Lex` `NonemptyInterval` `instLELex` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex` `toProd`	—	—
`toLex_lt_toLex` 📖	mathematical	—	`Lex` `NonemptyInterval` `instLTLex` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex` `toProd`	—	—
`toLex_mono` 📖	mathematical	—	`Monotone` `NonemptyInterval` `Preorder.toLE` `PartialOrder.toPreorder` `Lex` `instPreorder` `instPreorderLex` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex`	—	`Monotone.comp` `Prod.Lex.toLex_mono` `toDualProd_mono`
`toLex_strictMono` 📖	mathematical	—	`StrictMono` `NonemptyInterval` `Preorder.toLE` `PartialOrder.toPreorder` `Lex` `instPreorder` `instPreorderLex` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex`	—	`StrictMono.comp` `Prod.Lex.toLex_strictMono` `toDualProd_strictMono`

---

← Back to Index