Documentation Verification Report

WellOrderInductionData

📁 Source: Mathlib/CategoryTheory/SmallObject/WellOrderInductionData.lean

Statistics

Metric	Count
Definitions `WellOrderInductionData`, `instUnique`, `limit`, `ofLE`, `succ`, `val`, `zero`, `ofExists`, `sectionsMk`, `succ`	10
Theorems `compatibility`, `instNonempty`, `instSubsingletonOfWellFoundedLT`, `map_limit`, `map_succ`, `map_zero`, `ofLE_val`, `val_injective`, `zero_val`, `map_lift`, `map_succ`, `sectionsMk_val_op_bot`, `surjective`	13
Total	23

CategoryTheory.Functor

Definitions

Name	Category	Theorems
`WellOrderInductionData` 📖	CompData	—

CategoryTheory.Functor.WellOrderInductionData

Definitions

Name	Category	Theorems
`ofExists` 📖	CompOp	—
`sectionsMk` 📖	CompOp	1 math math: `sectionsMk_val_op_bot`
`succ` 📖	CompOp	2 math math: `map_succ`, `Extension.map_succ`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_lift` 📖	mathematical	`Order.IsSuccLimit` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Preorder.toLT`	`CategoryTheory.Functor.map` `Opposite` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `CategoryTheory.types` `Opposite.op` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.homOfLE` `LT.lt.le` `lift` `Set` `Set.instMembership` `CategoryTheory.Functor.sections` `Set.Iio` `Subtype.preorder` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.op` `Monotone.functor` `DFunLike.coe` `OrderHom` `OrderHom.instFunLike` `OrderHom.Subtype.val` `OrderHom.monotone`	—	—
`map_succ` 📖	mathematical	`IsMax` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`CategoryTheory.Functor.map` `Opposite` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `CategoryTheory.types` `Opposite.op` `Order.succ` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.homOfLE` `Order.le_succ` `succ`	—	—
`sectionsMk_val_op_bot` 📖	mathematical	—	`Set` `Set.instMembership` `CategoryTheory.Functor.sections` `Opposite` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `sectionsMk` `Opposite.op` `Bot.bot` `OrderBot.toBot` `Preorder.toLE`	—	`bot_le` `CategoryTheory.FunctorToTypes.map_id_apply` `Extension.map_zero`
`surjective` 📖	mathematical	—	`Set.Elem` `CategoryTheory.Functor.sections` `Opposite` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `CategoryTheory.Functor.obj` `CategoryTheory.types` `Opposite.op` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `Set` `Set.instMembership`	—	`sectionsMk_val_op_bot`

CategoryTheory.Functor.WellOrderInductionData.Extension

Definitions

Name	Category	Theorems
`instUnique` 📖	CompOp	—
`limit` 📖	CompOp	—
`ofLE` 📖	CompOp	1 math math: `ofLE_val`
`succ` 📖	CompOp	—
`val` 📖	CompOp	6 math math: `ofLE_val`, `map_zero`, `map_succ`, `compatibility`, `map_limit`, `zero_val`
`zero` 📖	CompOp	1 math math: `zero_val`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compatibility` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`CategoryTheory.Functor.map` `Opposite` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `CategoryTheory.types` `Opposite.op` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.homOfLE` `val`	—	`instSubsingletonOfWellFoundedLT`
`instNonempty` 📖	mathematical	—	`CategoryTheory.Functor.WellOrderInductionData.Extension`	—	—
`instSubsingletonOfWellFoundedLT` 📖	mathematical	—	`CategoryTheory.Functor.WellOrderInductionData.Extension`	—	`val_injective` `bot_le` `map_zero` `CategoryTheory.FunctorToTypes.map_id_apply` `Order.succ_le_of_lt` `Order.lt_succ_of_not_isMax` `not_isMax_iff` `LT.lt.le` `map_succ` `Order.le_succ` `le_refl` `OrderHom.monotone` `LE.le.trans` `map_limit`
`map_limit` 📖	mathematical	`Order.IsSuccLimit` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Preorder.toLE`	`CategoryTheory.Functor.map` `Opposite` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `CategoryTheory.types` `Opposite.op` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.homOfLE` `val` `CategoryTheory.Functor.WellOrderInductionData.lift` `Set` `Set.instMembership` `CategoryTheory.Functor.sections` `Set.Iio` `Subtype.preorder` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.op` `Monotone.functor` `DFunLike.coe` `OrderHom` `OrderHom.instFunLike` `OrderHom.Subtype.val` `OrderHom.monotone` `CategoryTheory.Functor.obj` `LE.le.trans` `LT.lt.le`	—	—
`map_succ` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`CategoryTheory.Functor.map` `Opposite` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `CategoryTheory.types` `Opposite.op` `Order.succ` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.homOfLE` `Order.succ_le_of_lt` `val` `CategoryTheory.Functor.WellOrderInductionData.succ` `IsMax` `Preorder.toLE` `not_isMax_iff` `LT.lt.le`	—	—
`map_zero` 📖	mathematical	—	`CategoryTheory.Functor.map` `Opposite` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `CategoryTheory.types` `Opposite.op` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.homOfLE` `bot_le` `val`	—	—
`ofLE_val` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`val` `ofLE` `CategoryTheory.Functor.map` `Opposite` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `CategoryTheory.types` `Opposite.op` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.homOfLE`	—	—
`val_injective` 📖	—	`val`	—	—	`bot_le` `Order.succ_le_of_lt` `not_isMax_iff` `LT.lt.le` `OrderHom.monotone` `LE.le.trans`
`zero_val` 📖	mathematical	—	`val` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `zero`	—	—

---

← Back to Index