Documentation Verification Report

WellFounded

📁 Source: Mathlib/Data/Finsupp/WellFounded.lean

Statistics

Metric	Count
Definitions	0
Theorems `wellFoundedLT`, `wellFoundedLT_of_finite`, `acc`, `wellFounded`, `wellFounded'`, `wellFoundedLT`, `wellFoundedLT_of_finite`, `wellFounded_of_finite`, `wellFoundedLT`, `wellFoundedLT'`, `wellFoundedLT_of_finite`	11
Total	11

Finsupp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`wellFoundedLT` 📖	mathematical	`Preorder.toLT`	`WellFoundedLT` `Finsupp` `preorder`	—	`IsWellFounded.wf` `DFinsupp.wellFoundedLT`
`wellFoundedLT'` 📖	mathematical	—	`WellFoundedLT` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Preorder.toLT` `preorder` `PartialOrder.toPreorder`	—	`wellFoundedLT` `LE.le.not_gt` `zero_le`
`wellFoundedLT_of_finite` 📖	mathematical	—	`WellFoundedLT` `Finsupp` `Preorder.toLT` `preorder`	—	`IsWellFounded.wf` `Function.wellFoundedLT`

Finsupp.Colex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`wellFoundedLT` 📖	mathematical	—	`WellFoundedLT` `Colex` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Finsupp.instLTColex` `Preorder.toLT` `PartialOrder.toPreorder`	—	`Finsupp.Lex.wellFoundedLT` `OrderDual.instTrichotomousLt` `instWellFoundedGTOrderDualOfWellFoundedLT`
`wellFoundedLT_of_finite` 📖	mathematical	—	`WellFoundedLT` `Colex` `Finsupp` `Finsupp.instLTColex` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`Finsupp.Lex.wellFoundedLT_of_finite` `OrderDual.finite`

Finsupp.Lex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`acc` 📖	mathematical	`Pi.instMinForall_mathlib` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `Prop.instCompleteLinearOrder` `Compl.compl` `Pi.instCompl` `Prop.instCompl`	`Finsupp` `Finsupp.Lex`	—	`Finsupp.lex_eq_invImage_dfinsupp_lex` `DFinsupp.Lex.acc` `toDFinsupp_support`
`wellFounded` 📖	mathematical	`Pi.instMinForall_mathlib` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `Prop.instCompleteLinearOrder` `Compl.compl` `Pi.instCompl` `Prop.instCompl`	`Finsupp` `Finsupp.Lex`	—	`acc`
`wellFounded'` 📖	mathematical	`Function.swap`	`Finsupp` `Finsupp.Lex`	—	`DFinsupp.Lex.wellFounded'` `Finsupp.lex_eq_invImage_dfinsupp_lex`
`wellFoundedLT` 📖	mathematical	—	`WellFoundedLT` `Lex` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Finsupp.instLTLex` `Preorder.toLT` `PartialOrder.toPreorder`	—	`wellFounded'` `LE.le.not_gt` `zero_le` `IsWellFounded.wf`
`wellFoundedLT_of_finite` 📖	mathematical	—	`WellFoundedLT` `Lex` `Finsupp` `Finsupp.instLTLex` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`wellFounded_of_finite` `instIsStrictTotalOrderLt` `IsWellFounded.wf`
`wellFounded_of_finite` 📖	mathematical	—	`Finsupp` `Finsupp.Lex`	—	`Pi.Lex.wellFounded`

---

← Back to Index