Documentation Verification Report

Order

📁 Source: Mathlib/Order/Hom/Order.lean

Statistics

Metric	Count
Definitions `instBotOfOrderBot`, `instCompleteLattice`, `instInfSet`, `instMax`, `instMin`, `instSemilatticeInf`, `instSemilatticeSup`, `instSupSet`, `instTopOrderHom`, `lattice`, `orderBot`, `orderTop`	12
Theorems `bot_def`, `coe_iInf`, `coe_iSup`, `coe_inf`, `coe_sup`, `iInf_apply`, `iSup_apply`, `iterate_sup_le_sup_iff`, `sInf_apply`, `sSup_apply`, `top_def`	11
Total	23

OrderHom

Definitions

Name	Category	Theorems
`instBotOfOrderBot` 📖	CompOp	1 math math: `bot_def`
`instCompleteLattice` 📖	CompOp	—
`instInfSet` 📖	CompOp	3 math math: `iInf_apply`, `coe_iInf`, `sInf_apply`
`instMax` 📖	CompOp	1 math math: `coe_sup`
`instMin` 📖	CompOp	2 math math: `gfp_const_inf_le`, `coe_inf`
`instSemilatticeInf` 📖	CompOp	—
`instSemilatticeSup` 📖	CompOp	—
`instSupSet` 📖	CompOp	3 math math: `sSup_apply`, `iSup_apply`, `coe_iSup`
`instTopOrderHom` 📖	CompOp	1 math math: `top_def`
`lattice` 📖	CompOp	—
`orderBot` 📖	CompOp	—
`orderTop` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bot_def` 📖	mathematical	—	`Bot.bot` `OrderHom` `instBotOfOrderBot` `DFunLike.coe` `instPreorder` `instFunLike` `const` `OrderBot.toBot` `Preorder.toLE`	—	—
`coe_iInf` 📖	mathematical	—	`DFunLike.coe` `OrderHom` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `instFunLike` `iInf` `instInfSet` `Pi.infSet` `CompleteSemilatticeInf.toInfSet`	—	`iInf_apply` `iInf_apply`
`coe_iSup` 📖	mathematical	—	`DFunLike.coe` `OrderHom` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `instFunLike` `iSup` `instSupSet` `Pi.supSet` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup`	—	`iSup_apply` `iSup_apply`
`coe_inf` 📖	mathematical	—	`DFunLike.coe` `OrderHom` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `instFunLike` `instMin` `Pi.instMinForall_mathlib` `SemilatticeInf.toMin`	—	—
`coe_sup` 📖	mathematical	—	`DFunLike.coe` `OrderHom` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `instFunLike` `instMax` `Pi.instMaxForall_mathlib` `SemilatticeSup.toMax`	—	—
`iInf_apply` 📖	mathematical	—	`DFunLike.coe` `OrderHom` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `instFunLike` `iInf` `instInfSet` `CompleteSemilatticeInf.toInfSet`	—	`sInf_apply` `iInf_range`
`iSup_apply` 📖	mathematical	—	`DFunLike.coe` `OrderHom` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `instFunLike` `iSup` `instSupSet` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup`	—	`sSup_apply` `iSup_range`
`iterate_sup_le_sup_iff` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Nat.iterate` `DFunLike.coe` `OrderHom` `instFunLike` `SemilatticeSup.toMax`	—	`le_refl` `Function.iterate_succ_apply` `Monotone.iterate` `mono` `Function.iterate_add_apply` `sup_comm`
`sInf_apply` 📖	mathematical	—	`DFunLike.coe` `OrderHom` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `instFunLike` `InfSet.sInf` `instInfSet` `iInf` `CompleteSemilatticeInf.toInfSet` `Set` `Set.instMembership`	—	—
`sSup_apply` 📖	mathematical	—	`DFunLike.coe` `OrderHom` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `instFunLike` `SupSet.sSup` `instSupSet` `iSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `Set` `Set.instMembership`	—	—
`top_def` 📖	mathematical	—	`Top.top` `OrderHom` `instTopOrderHom` `DFunLike.coe` `instPreorder` `instFunLike` `const` `OrderTop.toTop` `Preorder.toLE`	—	—

---

← Back to Index