Documentation Verification Report

TransfiniteIteration

📁 Source: Mathlib/Order/TransfiniteIteration.lean

Statistics

Metric	Count
Definitions `transfiniteIterate`	1
Theorems `monotone_transfiniteIterate`, `top_mem_range_transfiniteIterate`, `transfiniteIterate_bot`, `transfiniteIterate_limit`, `transfiniteIterate_succ`	5
Total	6

(root)

Definitions

Name	Category	Theorems
`transfiniteIterate` 📖	CompOp	8 math math: `monotone_transfiniteIterate`, `CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.exists_ordinal`, `transfiniteIterate_succ`, `transfiniteIterate_bot`, `CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.functorToMonoOver_map`, `CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.top_mem_range`, `CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.functorToMonoOver_obj`, `transfiniteIterate_limit`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`monotone_transfiniteIterate` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice`	`Monotone` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `transfiniteIterate` `ConditionallyCompletePartialOrderSup.toSupSet`	—	`le_refl` `IsMin.eq_bot` `LE.le.lt_or_eq` `LE.le.trans` `Order.lt_succ_iff_of_not_isMax` `transfiniteIterate_succ` `transfiniteIterate_limit` `le_iSup`
`top_mem_range_transfiniteIterate` 📖	—	`Preorder.toLT` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Top.top` `OrderTop.toTop` `Preorder.toLE` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `transfiniteIterate` `ConditionallyCompletePartialOrderSup.toSupSet`	—	—	`le_refl` `LT.lt.le` `lt_of_lt_of_le` `transfiniteIterate_succ` `monotone_transfiniteIterate` `Order.succ_le_of_lt`
`transfiniteIterate_bot` 📖	mathematical	—	`transfiniteIterate` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`SuccOrder.limitRecOn_isMin`
`transfiniteIterate_limit` 📖	mathematical	`Order.IsSuccLimit` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`transfiniteIterate` `iSup` `Set.Elem` `Set.Iio` `Set` `Set.instMembership`	—	`SuccOrder.limitRecOn_of_isSuccLimit` `iSup_apply`
`transfiniteIterate_succ` 📖	mathematical	`IsMax` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`transfiniteIterate` `Order.succ`	—	`SuccOrder.limitRecOn_succ_of_not_isMax`

---

← Back to Index