Documentation Verification Report

CompleteLinearOrder

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

Statistics

Metric	Count
Definitions `CompleteLinearOrder`, `toSuccOrder`	2
Theorems `exists_of_nonempty_of_not_isPredPrelimit`, `mem_of_nonempty_of_not_isPredPrelimit`, `exists_of_nonempty_of_not_isSuccPrelimit`, `mem_of_nonempty_of_not_isSuccPrelimit`, `iSup_Iio`, `sSup_Iio`, `iSup_Iio`, `sSup_Iio`, `csInf_mem_of_not_isPredPrelimit`, `csSup_mem_of_not_isSuccPrelimit`, `csSup_mem_of_not_isSuccPrelimit'`, `exists_eq_ciInf_of_not_isPredPrelimit`, `exists_eq_ciSup_of_not_isSuccPrelimit`, `exists_eq_ciSup_of_not_isSuccPrelimit'`, `exists_eq_iInf_of_not_isPredPrelimit`, `exists_eq_iSup_of_not_isSuccPrelimit`, `iSup_Iio_eq_self_iff_isSuccPrelimit`, `iSup_succ`, `sInf_mem_of_not_isPredPrelimit`, `sSup_Iio_eq_self_iff_isSuccPrelimit`, `sSup_mem_of_not_isSuccPrelimit`	21
Total	23

ConditionallyCompleteLinearOrder

Definitions

Name	Category	Theorems
`toSuccOrder` 📖	CompOp	—

IsGLB

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_of_nonempty_of_not_isPredPrelimit` 📖	—	`IsGLB` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `Set.range` `Order.IsPredPrelimit` `Preorder.toLT`	—	—	`mem_of_nonempty_of_not_isPredPrelimit` `Set.range_nonempty`
`mem_of_nonempty_of_not_isPredPrelimit` 📖	mathematical	`IsGLB` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `Set.Nonempty` `Order.IsPredPrelimit` `Preorder.toLT`	`Set` `Set.instMembership`	—	`csInf_mem_of_not_isPredPrelimit` `bddBelow` `csInf_eq`

IsLUB

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_of_nonempty_of_not_isSuccPrelimit` 📖	—	`IsLUB` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `Set.range` `Order.IsSuccPrelimit` `Preorder.toLT`	—	—	`mem_of_nonempty_of_not_isSuccPrelimit` `Set.range_nonempty`
`mem_of_nonempty_of_not_isSuccPrelimit` 📖	mathematical	`IsLUB` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `Set.Nonempty` `Order.IsSuccPrelimit` `Preorder.toLT`	`Set` `Set.instMembership`	—	`csSup_mem_of_not_isSuccPrelimit` `bddAbove` `csSup_eq`

Order.IsSuccLimit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`iSup_Iio` 📖	mathematical	`Order.IsSuccLimit` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder`	`iSup` `Set.Elem` `Set.Iio` `ConditionallyCompletePartialOrderSup.toSupSet` `Set` `Set.instMembership`	—	`Order.IsSuccPrelimit.iSup_Iio` `isSuccPrelimit`
`sSup_Iio` 📖	mathematical	`Order.IsSuccLimit` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder`	`SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet` `Set.Iio`	—	`Order.IsSuccPrelimit.sSup_Iio` `isSuccPrelimit`

Order.IsSuccPrelimit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`iSup_Iio` 📖	mathematical	`Order.IsSuccPrelimit` `Preorder.toLT` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder`	`iSup` `Set.Elem` `Set.Iio` `ConditionallyCompletePartialOrderSup.toSupSet` `Set` `Set.instMembership`	—	`sSup_eq_iSup'` `sSup_Iio`
`sSup_Iio` 📖	mathematical	`Order.IsSuccPrelimit` `Preorder.toLT` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder`	`SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet` `Set.Iio`	—	`eq_bot_or_bot_lt` `IsMin.Iio_eq` `csSup_empty` `IsLUB.csSup_eq` `isLUB_Iio`

(root)

Definitions

Name	Category	Theorems
`CompleteLinearOrder` 📖	CompData	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`csInf_mem_of_not_isPredPrelimit` 📖	mathematical	`Set.Nonempty` `BddBelow` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `Order.IsPredPrelimit` `Preorder.toLT` `InfSet.sInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf`	`Set` `Set.instMembership`	—	`not_forall_not` `exists_lt_of_csInf_lt` `CovBy.lt` `eq_of_le_of_not_lt` `csInf_le`
`csSup_mem_of_not_isSuccPrelimit` 📖	mathematical	`Set.Nonempty` `BddAbove` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `Order.IsSuccPrelimit` `Preorder.toLT` `SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet`	`Set` `Set.instMembership`	—	`not_forall_not` `exists_lt_of_lt_csSup` `CovBy.lt` `eq_of_le_of_not_lt` `le_csSup`
`csSup_mem_of_not_isSuccPrelimit'` 📖	mathematical	`BddAbove` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `Order.IsSuccPrelimit` `Preorder.toLT` `SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet`	`Set` `Set.instMembership`	—	`Set.eq_empty_or_nonempty` `csSup_empty` `csSup_mem_of_not_isSuccPrelimit`
`exists_eq_ciInf_of_not_isPredPrelimit` 📖	—	`BddBelow` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `Set.range` `Order.IsPredPrelimit` `Preorder.toLT` `iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf`	—	—	`csInf_mem_of_not_isPredPrelimit` `Set.range_nonempty`
`exists_eq_ciSup_of_not_isSuccPrelimit` 📖	—	`BddAbove` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `Set.range` `Order.IsSuccPrelimit` `Preorder.toLT` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet`	—	—	`csSup_mem_of_not_isSuccPrelimit` `Set.range_nonempty`
`exists_eq_ciSup_of_not_isSuccPrelimit'` 📖	—	`BddAbove` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `Set.range` `Order.IsSuccPrelimit` `Preorder.toLT` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet`	—	—	`csSup_mem_of_not_isSuccPrelimit'`
`exists_eq_iInf_of_not_isPredPrelimit` 📖	—	`Order.IsPredPrelimit` `Preorder.toLT` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf`	—	—	`sInf_mem_of_not_isPredPrelimit`
`exists_eq_iSup_of_not_isSuccPrelimit` 📖	—	`Order.IsSuccPrelimit` `Preorder.toLT` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet`	—	—	`sSup_mem_of_not_isSuccPrelimit`
`iSup_Iio_eq_self_iff_isSuccPrelimit` 📖	mathematical	—	`iSup` `Set.Elem` `Set.Iio` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `ConditionallyCompletePartialOrderSup.toSupSet` `Set` `Set.instMembership` `Order.IsSuccPrelimit` `Preorder.toLT`	—	`sSup_eq_iSup'` `sSup_Iio_eq_self_iff_isSuccPrelimit`
`iSup_succ` 📖	mathematical	—	`iSup` `Set.Elem` `Set.Iio` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `ConditionallyCompletePartialOrderSup.toSupSet` `Order.succ` `Set` `Set.instMembership`	—	`le_antisymm` `ciSup_le_iff'` `Order.succ_le_of_lt` `le_of_forall_lt` `lt_ciSup_iff'` `Order.lt_succ_of_not_isMax` `LT.lt.not_isMax`
`sInf_mem_of_not_isPredPrelimit` 📖	mathematical	`Order.IsPredPrelimit` `Preorder.toLT` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `InfSet.sInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf`	`Set` `Set.instMembership`	—	`not_forall_not` `sInf_lt_iff` `CovBy.lt` `eq_of_le_of_not_lt` `sInf_le`
`sSup_Iio_eq_self_iff_isSuccPrelimit` 📖	mathematical	—	`SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `Set.Iio` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `Order.IsSuccPrelimit` `Preorder.toLT`	—	`csSup_mem_of_not_isSuccPrelimit'` `bddAbove_Iio` `Order.IsSuccPrelimit.sSup_Iio`
`sSup_mem_of_not_isSuccPrelimit` 📖	mathematical	`Order.IsSuccPrelimit` `Preorder.toLT` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet`	`Set` `Set.instMembership`	—	`not_forall_not` `lt_sSup_iff` `CovBy.lt` `eq_of_le_of_not_lt` `le_sSup`

---

← Back to Index