Documentation Verification Report

WithBot

📁 Source: Mathlib/Order/SuccPred/WithBot.lean

Statistics

Metric	Count
Definitions `succ`, `pred`	2
Theorems `lt_succ`, `succ_bot`, `succ_coe`, `succ_eq_bot`, `succ_eq_succ`, `succ_le_succ`, `succ_lt_succ`, `succ_mono`, `succ_strictMono`, `pred_coe`, `pred_eq_pred`, `pred_eq_top`, `pred_le_pred`, `pred_lt_pred`, `pred_mono`, `pred_strictMono`, `pred_top`	17
Total	19

WithBot

Definitions

Name	Category	Theorems
`succ` 📖	CompOp	19 math math: `Polynomial.length_coeffList_eq_withBotSucc_degree`, `lt_succ`, `Order.succ_eq_zero`, `succ_eq_bot`, `succ_coe`, `Polynomial.coeffList_eraseLead`, `succ_mono`, `succ_one`, `withBotSucc_zero`, `withBotSucc_one`, `succ_zero`, `succ_bot`, `succ_natCast`, `succ_le_succ`, `Polynomial.withBotSucc_degree_eq_natDegree_add_one`, `succ_eq_succ`, `succ_strictMono`, `succ_ofNat`, `succ_lt_succ`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`lt_succ` 📖	mathematical	—	`WithBot` `Preorder.toLT` `instPreorder` `some` `succ`	—	`Order.lt_succ` `noMaxOrder` `bot_nonempty` `succ_eq_succ`
`succ_bot` 📖	mathematical	—	`succ` `Bot.bot` `WithBot` `bot` `OrderBot.toBot` `Preorder.toLE`	—	—
`succ_coe` 📖	mathematical	—	`succ` `some` `Order.succ`	—	—
`succ_eq_bot` 📖	mathematical	—	`succ` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `WithBot` `bot`	—	`ne_of_gt` `le_bot_iff` `LE.le.trans` `Order.le_succ` `not_isMax_bot` `Order.max_of_succ_le` `bot_le`
`succ_eq_succ` 📖	mathematical	—	`some` `succ` `Order.succ` `WithBot` `instPreorder` `instSuccOrder`	—	—
`succ_le_succ` 📖	mathematical	`WithBot` `Preorder.toLE` `instPreorder`	`succ`	—	`succ_mono`
`succ_lt_succ` 📖	mathematical	`WithBot` `Preorder.toLT` `instPreorder`	`succ`	—	`succ_strictMono`
`succ_mono` 📖	mathematical	—	`Monotone` `WithBot` `instPreorder` `succ`	—	`Order.succ_le_succ`
`succ_strictMono` 📖	mathematical	—	`StrictMono` `WithBot` `instPreorder` `succ`	—	`Order.succ_lt_succ`

WithTop

Definitions

Name	Category	Theorems
`pred` 📖	CompOp	8 math math: `pred_eq_pred`, `pred_coe`, `pred_eq_top`, `pred_mono`, `pred_strictMono`, `pred_top`, `pred_le_pred`, `pred_lt_pred`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`pred_coe` 📖	mathematical	—	`pred` `some` `Order.pred`	—	—
`pred_eq_pred` 📖	mathematical	—	`some` `pred` `Order.pred` `WithTop` `instPreorder` `instPredOrder`	—	—
`pred_eq_top` 📖	mathematical	—	`pred` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Top.top` `OrderTop.toTop` `Preorder.toLE` `WithTop` `top`	—	`ne_of_lt` `top_le_iff` `LE.le.trans` `Order.pred_le` `not_isMin_top` `Order.min_of_le_pred` `le_top`
`pred_le_pred` 📖	mathematical	`WithTop` `Preorder.toLE` `instPreorder`	`pred`	—	`pred_mono`
`pred_lt_pred` 📖	mathematical	`WithTop` `Preorder.toLT` `instPreorder`	`pred`	—	`pred_strictMono`
`pred_mono` 📖	mathematical	—	`Monotone` `WithTop` `instPreorder` `pred`	—	`Order.pred_le_pred`
`pred_strictMono` 📖	mathematical	—	`StrictMono` `WithTop` `instPreorder` `pred`	—	`Order.pred_lt_pred`
`pred_top` 📖	mathematical	—	`pred` `Top.top` `WithTop` `top` `OrderTop.toTop` `Preorder.toLE`	—	—

---

← Back to Index