Documentation Verification Report

WellFounded

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

Statistics

Metric	Count
Definitions	0
Theorems `wellFoundedLT`, `wellFoundedLT_of_finite`, `acc`, `acc_of_single`, `acc_of_single_erase`, `acc_single`, `acc_zero`, `wellFounded`, `wellFounded'`, `wellFoundedLT`, `wellFoundedLT_of_finite`, `wellFounded_of_finite`, `lex_fibration`, `wellFoundedLT`, `wellFoundedLT'`, `wellFoundedLT_of_finite`, `wellFoundedLT`, `wellFoundedLT`, `wellFoundedLT`, `wellFounded`, `wellFoundedLT`, `wellFoundedLT`	22
Total	22

DFinsupp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`lex_fibration` 📖	mathematical	—	`Relation.Fibration` `Set` `DFinsupp` `Prod.GameAdd` `Lex` `piecewise`	—	`ext`
`wellFoundedLT` 📖	mathematical	`WellFoundedLT` `Preorder.toLT`	`DFinsupp` `instPreorder`	—	`instIsPreorderLe` `Std.Trichotomous.swap` `IsWellOrder.toTrichotomous` `WellOrderingRel.isWellOrder` `Lex.wellFounded'` `IsWellFounded.wf` `instWellFoundedLTAntisymmetrizationLe` `IsWellOrder.toIsWellFounded` `IsStrictOrder.swap` `IsStrictTotalOrder.toIsStrictOrder` `instIsStrictTotalOrderOfIsWellOrder` `lex_lt_of_lt_of_preorder`
`wellFoundedLT'` 📖	mathematical	`CanonicallyOrderedAdd` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `Preorder.toLE` `PartialOrder.toPreorder` `WellFoundedLT` `Preorder.toLT`	`DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instPreorder`	—	`wellFoundedLT` `LE.le.not_gt` `zero_le`
`wellFoundedLT_of_finite` 📖	mathematical	`WellFoundedLT` `Preorder.toLT`	`DFinsupp` `instPreorder`	—	`IsWellFounded.wf` `Pi.wellFoundedLT`

DFinsupp.Colex

Theorems

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

DFinsupp.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`	`DFinsupp` `DFinsupp.Lex`	—	`acc_of_single` `acc_single`
`acc_of_single` 📖	—	`DFinsupp` `DFinsupp.Lex` `DFinsupp.single` `DFunLike.coe` `DFinsupp.instDFunLike`	—	—	`Finset.induction` `DFinsupp.support_eq_empty` `acc_zero` `acc_of_single_erase` `Finset.mem_insert_self` `DFinsupp.support_erase` `Finset.erase_insert` `DFinsupp.erase_ne` `Membership.mem.ne_of_notMem` `Finset.mem_insert_of_mem`
`acc_of_single_erase` 📖	—	`DFinsupp` `DFinsupp.Lex` `DFinsupp.single` `DFunLike.coe` `DFinsupp.instDFunLike` `DFinsupp.erase`	—	—	`Lean.Meta.FastSubsingleton.elim` `Lean.Meta.instFastSubsingletonForall` `Lean.Meta.instFastSubsingletonDecidable` `DFinsupp.piecewise_single_erase` `Acc.of_fibration` `DFinsupp.lex_fibration` `Acc.prod_gameAdd`
`acc_single` 📖	mathematical	`Pi.instMinForall_mathlib` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `Prop.instCompleteLinearOrder` `Compl.compl` `Pi.instCompl` `Prop.instCompl`	`DFinsupp` `DFinsupp.Lex` `DFinsupp.single`	—	`acc_of_single` `eq_or_ne` `DFinsupp.single_eq_of_ne` `DFinsupp.single_zero` `acc_zero` `DFinsupp.single_apply`
`acc_zero` 📖	mathematical	—	`DFinsupp` `DFinsupp.Lex` `DFinsupp.instZero`	—	—
`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`	`DFinsupp` `DFinsupp.Lex`	—	`acc`
`wellFounded'` 📖	mathematical	`Function.swap`	`DFinsupp` `DFinsupp.Lex`	—	`wellFounded` `Not.imp_symm`
`wellFoundedLT` 📖	mathematical	`CanonicallyOrderedAdd` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `Preorder.toLE` `PartialOrder.toPreorder` `WellFoundedLT` `Preorder.toLT`	`Lex` `DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DFinsupp.instLTLex`	—	`wellFounded'` `LE.le.not_gt` `zero_le` `IsWellFounded.wf`
`wellFoundedLT_of_finite` 📖	mathematical	`WellFoundedLT`	`Lex` `DFinsupp` `DFinsupp.instLTLex` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`wellFounded_of_finite` `instIsStrictTotalOrderLt` `IsWellFounded.wf`
`wellFounded_of_finite` 📖	mathematical	—	`DFinsupp` `DFinsupp.Lex`	—	`Pi.Lex.wellFounded`

Function

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`wellFoundedLT` 📖	mathematical	—	`WellFoundedLT` `Preorder.toLT` `Pi.preorder`	—	`Pi.wellFoundedLT`

Function.Lex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`wellFoundedLT` 📖	mathematical	—	`WellFoundedLT` `Lex` `Pi.instLTLexForall` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`Pi.Lex.wellFoundedLT`

Pi

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`wellFoundedLT` 📖	mathematical	`WellFoundedLT` `Preorder.toLT`	`preorder`	—	`isEmpty_or_nonempty` `Lean.Meta.FastSubsingleton.elim` `Lean.Meta.instFastSubsingletonForall` `Lean.Meta.instFastSubsingletonForallOfFastIsEmpty` `IsWellFounded.wf` `DFinsupp.wellFoundedLT` `WellFounded.not_lt_min`

Pi.Colex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`wellFoundedLT` 📖	mathematical	`WellFoundedLT`	`Colex` `Pi.instLTColexForall` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`Pi.Lex.wellFoundedLT` `OrderDual.finite`

Pi.Lex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`wellFounded` 📖	mathematical	—	`Pi.Lex`	—	`isEmpty_or_nonempty` `Lean.Meta.FastSubsingleton.elim` `Lean.Meta.instFastSubsingletonForall` `Lean.Meta.instFastSubsingletonForallOfFastIsEmpty` `DFinsupp.Lex.wellFounded'` `WellFounded.not_lt_min` `IsStrictTotalOrder.toTrichotomous` `Finite.wellFounded_of_trans_of_irrefl` `IsTrans.swap` `IsStrictOrder.toIsTrans` `IsStrictTotalOrder.toIsStrictOrder` `Std.Irrefl.swap` `IsStrictOrder.toIrrefl`
`wellFoundedLT` 📖	mathematical	`WellFoundedLT`	`Lex` `Pi.instLTLexForall` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`wellFounded` `instIsStrictTotalOrderLt` `IsWellFounded.wf`

---

← Back to Index