Documentation Verification Report

Well

📁 Source: Mathlib/Order/Extension/Well.lean

Statistics

Metric	Count
Definitions `wellOrderExtension`, `WellOrderExtension`, `instInhabitedWellOrderExtension`, `instLinearOrderWellOrderExtensionOfWellFoundedLT`, `toWellOrderExtension`	5
Theorems `exists_well_order_ge`, `isWellFounded_lt`, `isWellOrder_lt`, `wellFoundedLT`, `toWellOrderExtension_strictMono`	5
Total	10

IsWellFounded

Definitions

Name	Category	Theorems
`wellOrderExtension` 📖	CompOp	2 math math: `wellOrderExtension.isWellFounded_lt`, `wellOrderExtension.isWellOrder_lt`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_well_order_ge` 📖	mathematical	—	`Pi.hasLe` `Prop.le` `IsWellOrder`	—	`rank_lt_of_rel` `instTrichotomousLt` `instIsTransLt` `wellOrderExtension.isWellFounded_lt`

IsWellFounded.wellOrderExtension

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isWellFounded_lt` 📖	mathematical	—	`IsWellFounded` `Preorder.toLT` `PartialOrder.toPreorder` `LinearOrder.toPartialOrder` `IsWellFounded.wellOrderExtension`	—	`WellFounded.prod_lex` `Ordinal.lt_wf` `Cardinal.lt_wf`
`isWellOrder_lt` 📖	mathematical	—	`IsWellOrder` `Preorder.toLT` `PartialOrder.toPreorder` `LinearOrder.toPartialOrder` `IsWellFounded.wellOrderExtension`	—	`instTrichotomousLt` `instIsTransLt` `isWellFounded_lt`

WellOrderExtension

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`wellFoundedLT` 📖	mathematical	—	`WellFoundedLT` `WellOrderExtension` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderWellOrderExtensionOfWellFoundedLT`	—	`IsWellFounded.wellOrderExtension.isWellFounded_lt`

(root)

Definitions

Name	Category	Theorems
`WellOrderExtension` 📖	CompOp	2 math math: `WellOrderExtension.wellFoundedLT`, `toWellOrderExtension_strictMono`
`instInhabitedWellOrderExtension` 📖	CompOp	—
`instLinearOrderWellOrderExtensionOfWellFoundedLT` 📖	CompOp	2 math math: `WellOrderExtension.wellFoundedLT`, `toWellOrderExtension_strictMono`
`toWellOrderExtension` 📖	CompOp	1 math math: `toWellOrderExtension_strictMono`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toWellOrderExtension_strictMono` 📖	mathematical	—	`StrictMono` `WellOrderExtension` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderWellOrderExtensionOfWellFoundedLT` `Preorder.toLT` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toWellOrderExtension`	—	`IsWellFounded.rank_lt_of_rel`

---

← Back to Index