Limit

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

Statistics

Metric	Count
Definitions `IsPredLimit`, `IsPredPrelimit`, `IsSuccLimit`, `IsSuccPrelimit`, `mid`, `isPredLimitRecOn`, `isPredPrelimitRecOn`, `isSuccLimitRecOn`, `isSuccPrelimitRecOn`, `colimitRecOn`, `prelimitRecOn`, `limitRecOn`, `prelimitRecOn`	13
Theorems `isPredLimit_of_notMem`, `isPredPrelimit_of_notMem`, `mem_of_not_isPredLimit`, `mem_of_not_isPredPrelimit`, `isSuccLimit_of_notMem`, `isSuccPrelimit_of_notMem`, `mem_of_not_isSuccLimit`, `mem_of_not_isSuccPrelimit`, `isPredPrelimit`, `not_isPredLimit`, `isSuccPrelimit`, `not_isSuccLimit`, `dual`, `isGLB_Ioi`, `isMin`, `isPredPrelimit`, `le_iff_forall_le`, `lt_iff_exists_lt`, `lt_pred`, `lt_pred_iff`, `lt_top`, `ne_top`, `nonempty_Ioi`, `not_isMax`, `pred_le_iff`, `pred_ne`, `dual`, `isGLB_Ioi`, `isMax`, `isMax_of_noMin`, `isMin`, `isPredLimit`, `isPredLimit_of_not_isMax`, `le_iff_forall_le`, `lt_iff_exists_lt`, `lt_pred`, `lt_pred_iff`, `of_dense`, `pred_le_iff`, `pred_ne`, `bot_lt`, `dual`, `isLUB_Iio`, `isMax`, `isSuccPrelimit`, `le_iff_forall_le`, `le_succ_iff`, `lt_iff_exists_lt`, `ne_bot`, `nonempty_Iio`, `not_isMin`, `succ_lt`, `succ_lt_iff`, `succ_ne`, `dual`, `isLUB_Iio`, `isMax`, `isMin`, `isMin_of_noMax`, `isSuccLimit`, `isSuccLimit_of_not_isMin`, `le_iff_forall_le`, `le_succ_iff`, `lt_iff_exists_lt`, `of_dense`, `succ_lt`, `succ_lt_iff`, `succ_ne`, `isGLB_Ioi_iff_isPredPrelimit`, `isLUB_Iio_iff_isSuccPrelimit`, `isMax_or_mem_range_pred_or_isPredLimit`, `isMin_or_mem_range_succ_or_isSuccLimit`, `isPredLimitRecOn_of_isMax`, `isPredLimitRecOn_of_isPredLimit`, `isPredLimitRecOn_pred`, `isPredLimitRecOn_pred_of_not_isMin`, `isPredLimit_iff`, `isPredLimit_toDual_iff`, `isPredPrelimitRecOn_of_isPredPrelimit`, `isPredPrelimitRecOn_pred`, `isPredPrelimitRecOn_pred_of_not_isMin`, `isPredPrelimit_iff`, `isPredPrelimit_iff_isPredLimit`, `isPredPrelimit_iff_isPredLimit_of_not_isMax`, `isPredPrelimit_iff_lt_pred`, `isPredPrelimit_iff_of_noMin`, `isPredPrelimit_iff_pred_ne`, `isPredPrelimit_of_lt_pred`, `isPredPrelimit_of_pred_lt`, `isPredPrelimit_of_pred_ne`, `isPredPrelimit_toDual_iff`, `isPredPrelimit_top`, `isSuccLimitRecOn_of_isMin`, `isSuccLimitRecOn_of_isSuccLimit`, `isSuccLimitRecOn_succ`, `isSuccLimitRecOn_succ_of_not_isMax`, `isSuccLimit_iff`, `isSuccLimit_toDual_iff`, `isSuccPrelimitRecOn_of_isSuccPrelimit`, `isSuccPrelimitRecOn_succ`, `isSuccPrelimitRecOn_succ_of_not_isMax`, `isSuccPrelimit_bot`, `isSuccPrelimit_iff`, `isSuccPrelimit_iff_isSuccLimit`, `isSuccPrelimit_iff_isSuccLimit_of_not_isMin`, `isSuccPrelimit_iff_of_noMax`, `isSuccPrelimit_iff_succ_lt`, `isSuccPrelimit_iff_succ_ne`, `isSuccPrelimit_of_succ_lt`, `isSuccPrelimit_of_succ_ne`, `isSuccPrelimit_toDual_iff`, `mem_range_pred_of_not_isPredPrelimit`, `mem_range_pred_or_isPredPrelimit`, `mem_range_succ_of_not_isSuccPrelimit`, `mem_range_succ_or_isSuccPrelimit`, `not_isPredLimit`, `not_isPredLimit_iff`, `not_isPredLimit_of_noMin`, `not_isPredLimit_of_not_isPredPrelimit`, `not_isPredLimit_pred`, `not_isPredLimit_pred_of_not_isMin`, `not_isPredLimit_top`, `not_isPredPrelimit`, `not_isPredPrelimit_iff`, `not_isPredPrelimit_iff'`, `not_isPredPrelimit_iff_exists_covBy`, `not_isPredPrelimit_of_noMin`, `not_isPredPrelimit_pred`, `not_isPredPrelimit_pred_of_not_isMin`, `not_isSuccLimit`, `not_isSuccLimit_bot`, `not_isSuccLimit_iff`, `not_isSuccLimit_of_noMax`, `not_isSuccLimit_succ`, `not_isSuccLimit_succ_of_not_isMax`, `not_isSuccPrelimit`, `not_isSuccPrelimit_iff`, `not_isSuccPrelimit_iff'`, `not_isSuccPrelimit_iff_exists_covBy`, `not_isSuccPrelimit_of_noMax`, `not_isSuccPrelimit_succ`, `not_isSuccPrelimit_succ_of_not_isMax`, `colimitRecOn_isMax`, `colimitRecOn_of_isPredLimit`, `colimitRecOn_pred`, `colimitRecOn_pred_of_not_isMin`, `prelimitRecOn_of_isPredPrelimit`, `prelimitRecOn_pred`, `prelimitRecOn_pred_of_not_isMin`, `limitRecOn_isMin`, `limitRecOn_of_isSuccLimit`, `limitRecOn_succ`, `limitRecOn_succ_of_not_isMax`, `prelimitRecOn_of_isSuccPrelimit`, `prelimitRecOn_succ`, `prelimitRecOn_succ_of_not_isMax`	156
Total	169

IsGLB

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isPredLimit_of_notMem` 📖	mathematical	`IsGLB` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.Nonempty` `Set` `Set.instMembership`	`Order.IsPredLimit`	—	`IsLUB.isSuccLimit_of_notMem` `dual`
`isPredPrelimit_of_notMem` 📖	mathematical	`IsGLB` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set` `Set.instMembership`	`Order.IsPredPrelimit` `Preorder.toLT`	—	`IsLUB.isSuccPrelimit_of_notMem` `dual`
`mem_of_not_isPredLimit` 📖	mathematical	`IsGLB` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.Nonempty` `Order.IsPredLimit`	`Set` `Set.instMembership`	—	`Not.imp_symm` `isPredLimit_of_notMem`
`mem_of_not_isPredPrelimit` 📖	mathematical	`IsGLB` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Order.IsPredPrelimit` `Preorder.toLT`	`Set` `Set.instMembership`	—	`Not.imp_symm` `isPredPrelimit_of_notMem`

IsLUB

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isSuccLimit_of_notMem` 📖	mathematical	`IsLUB` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.Nonempty` `Set` `Set.instMembership`	`Order.IsSuccLimit`	—	`LE.le.eq_or_lt` `LT.lt.not_isMin` `isSuccPrelimit_of_notMem`
`isSuccPrelimit_of_notMem` 📖	mathematical	`IsLUB` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set` `Set.instMembership`	`Order.IsSuccPrelimit` `Preorder.toLT`	—	`exists_between` `CovBy.lt` `LE.le.antisymm` `CovBy.ge_of_gt`
`mem_of_not_isSuccLimit` 📖	mathematical	`IsLUB` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.Nonempty` `Order.IsSuccLimit`	`Set` `Set.instMembership`	—	`Not.imp_symm` `isSuccLimit_of_notMem`
`mem_of_not_isSuccPrelimit` 📖	mathematical	`IsLUB` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Order.IsSuccPrelimit` `Preorder.toLT`	`Set` `Set.instMembership`	—	`Not.imp_symm` `isSuccPrelimit_of_notMem`

IsMax

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isPredPrelimit` 📖	mathematical	`IsMax` `Preorder.toLE`	`Order.IsPredPrelimit` `Preorder.toLT`	—	`not_isMax_of_lt` `CovBy.lt`
`not_isPredLimit` 📖	mathematical	`IsMax` `Preorder.toLE`	`Order.IsPredLimit`	—	`Order.IsPredLimit.not_isMax`

IsMin

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isSuccPrelimit` 📖	mathematical	`IsMin` `Preorder.toLE`	`Order.IsSuccPrelimit` `Preorder.toLT`	—	`not_isMin_of_lt` `CovBy.lt`
`not_isSuccLimit` 📖	mathematical	`IsMin` `Preorder.toLE`	`Order.IsSuccLimit`	—	`Order.IsSuccLimit.not_isMin`

Order

Definitions

Name	Category	Theorems
`IsPredLimit` 📖	MathDef	21 math math: `isMax_or_mem_range_pred_or_isPredLimit`, `IsMax.not_isPredLimit`, `PredOrder.isPredLimit_of_mem_frontier`, `IsPredPrelimit.isPredLimit`, `not_isPredLimit_pred_of_not_isMin`, `not_isPredLimit`, `isPredPrelimit_iff_isPredLimit`, `IsSuccLimit.dual`, `PredOrder.nhds_eq_pure`, `isPredPrelimit_iff_isPredLimit_of_not_isMax`, `isPredLimit_toDual_iff`, `isSuccLimit_toDual_iff`, `not_isPredLimit_pred`, `not_isPredLimit_of_not_isPredPrelimit`, `isPredLimit_iff`, `not_isPredLimit_top`, `not_isPredLimit_iff`, `IsGLB.isPredLimit_of_notMem`, `PredOrder.isOpen_singleton_iff`, `IsPredPrelimit.isPredLimit_of_not_isMax`, `not_isPredLimit_of_noMin`
`IsPredPrelimit` 📖	MathDef	28 math math: `IsSuccPrelimit.dual`, `IsPredLimit.isPredPrelimit`, `not_isPredPrelimit_iff`, `not_isPredPrelimit_iff'`, `not_isPredPrelimit_of_noMin`, `not_isPredPrelimit`, `not_isPredPrelimit_pred_of_not_isMin`, `isPredPrelimit_of_pred_ne`, `isPredPrelimit_toDual_iff`, `isPredPrelimit_iff_isPredLimit`, `not_isPredPrelimit_pred`, `isPredPrelimit_iff`, `mem_range_pred_or_isPredPrelimit`, `isGLB_Ioi_iff_isPredPrelimit`, `not_isPredPrelimit_iff_exists_covBy`, `IsPredPrelimit.of_dense`, `isPredPrelimit_iff_of_noMin`, `isPredPrelimit_of_pred_lt`, `isPredPrelimit_iff_isPredLimit_of_not_isMax`, `isPredPrelimit_iff_pred_ne`, `isPredPrelimit_of_lt_pred`, `isPredPrelimit_top`, `isPredLimit_iff`, `IsGLB.isPredPrelimit_of_notMem`, `not_isPredLimit_iff`, `isSuccPrelimit_toDual_iff`, `isPredPrelimit_iff_lt_pred`, `IsMax.isPredPrelimit`
`IsSuccLimit` 📖	MathDef	47 math math: `Ordinal.isSuccLimit_lift`, `Ordinal.IsAcc.isSuccLimit`, `Cardinal.isStrongLimit_preBeth`, `Cardinal.isSuccLimit_ord`, `Ordinal.isOpen_singleton_iff`, `PrincipalSeg.isSuccLimit_apply_iff`, `Ordinal.isSuccLimit_omega0`, `not_isSuccLimit_of_noMax`, `Ordinal.isSuccLimit_add_iff`, `isMin_or_mem_range_succ_or_isSuccLimit`, `isSuccPrelimit_iff_isSuccLimit_of_not_isMin`, `SuccOrder.nhds_eq_pure`, `isSuccLimit_iff`, `Cardinal.IsStrongLimit.isSuccLimit`, `Ordinal.zero_or_succ_or_isSuccLimit`, `not_isSuccLimit_bot`, `IsPredLimit.dual`, `not_isSuccLimit`, `Ordinal.isSuccLimit_of_principal_add`, `Cardinal.isSuccLimit_aleph0`, `Ordinal.not_isSuccLimit_zero`, `Ordinal.isSuccLimit_iff`, `not_isSuccLimit_succ_of_not_isMax`, `Cardinal.not_isSuccLimit_natCast`, `isSuccPrelimit_iff_isSuccLimit`, `IsSuccPrelimit.isSuccLimit_of_not_isMin`, `isPredLimit_toDual_iff`, `not_isSuccLimit_iff`, `isSuccLimit_toDual_iff`, `Ordinal.aleph0_le_cof`, `Cardinal.isSuccLimit_iff`, `not_isSuccLimit_natCast`, `SuccOrder.isOpen_singleton_iff`, `SuccOrder.isSuccLimit_of_mem_frontier`, `ONote.fundamentalSequenceProp_inr`, `InitialSeg.isSuccLimit_apply_iff`, `IsLUB.isSuccLimit_of_notMem`, `IsMin.not_isSuccLimit`, `Cardinal.isSuccLimit_omega`, `Cardinal.not_isSuccLimit_of_lt_aleph0`, `Ordinal.isSuccLimit_of_principal_mul`, `Ordinal.isSuccLimit_of_mem_frontier`, `Ordinal.nhds_eq_pure`, `Ordinal.isSuccLimit_iff_omega0_dvd`, `IsSuccPrelimit.isSuccLimit`, `not_isSuccLimit_succ`, `Cardinal.not_isSuccLimit_zero`
`IsSuccPrelimit` 📖	MathDef	43 math math: `IsMin.isSuccPrelimit`, `sSup_Iio_eq_self_iff_isSuccPrelimit`, `mem_range_succ_or_isSuccPrelimit`, `not_isSuccPrelimit_succ_of_not_isMax`, `isSuccPrelimit_iff_succ_lt`, `Ordinal.isSuccLimit_add_iff_of_isSuccLimit`, `IsSuccPrelimit.of_dense`, `PrincipalSeg.isSuccPrelimit_apply_iff`, `not_isSuccPrelimit_iff_exists_covBy`, `isPredPrelimit_toDual_iff`, `isSuccPrelimit_iff_isSuccLimit_of_not_isMin`, `isSuccLimit_iff`, `isSuccPrelimit_iff`, `not_isSuccPrelimit_iff'`, `isSuccPrelimit_of_succ_ne`, `Ordinal.isSuccPrelimit_zero`, `not_isSuccPrelimit_of_noMax`, `isSuccPrelimit_bot`, `Cardinal.IsStrongLimit.isSuccPrelimit`, `Ordinal.pred_lt_iff_not_isSuccPrelimit`, `Cardinal.isStrongLimit_beth`, `isLUB_Iio_iff_isSuccPrelimit`, `Ordinal.isSuccLimit_iff`, `Ordinal.pred_eq_iff_isSuccPrelimit`, `isSuccPrelimit_iff_isSuccLimit`, `not_isSuccLimit_iff`, `IsPredPrelimit.dual`, `Ordinal.isSuccPrelimit_lift`, `Cardinal.isSuccLimit_iff`, `isSuccPrelimit_iff_succ_ne`, `IsLUB.isSuccPrelimit_of_notMem`, `iSup_Iio_eq_self_iff_isSuccPrelimit`, `IsSuccLimit.isSuccPrelimit`, `Cardinal.isSuccPrelimit_aleph0`, `Cardinal.isSuccPrelimit_zero`, `InitialSeg.isSuccPrelimit_apply_iff`, `isSuccPrelimit_toDual_iff`, `Ordinal.succ_pred_eq_iff_not_isSuccPrelimit`, `not_isSuccPrelimit_succ`, `not_isSuccPrelimit`, `not_isSuccPrelimit_iff`, `isSuccPrelimit_iff_of_noMax`, `isSuccPrelimit_of_succ_lt`
`isPredLimitRecOn` 📖	CompOp	4 math math: `isPredLimitRecOn_of_isPredLimit`, `isPredLimitRecOn_of_isMax`, `isPredLimitRecOn_pred`, `isPredLimitRecOn_pred_of_not_isMin`
`isPredPrelimitRecOn` 📖	CompOp	3 math math: `isPredPrelimitRecOn_pred_of_not_isMin`, `isPredPrelimitRecOn_pred`, `isPredPrelimitRecOn_of_isPredPrelimit`
`isSuccLimitRecOn` 📖	CompOp	4 math math: `isSuccLimitRecOn_succ_of_not_isMax`, `isSuccLimitRecOn_of_isSuccLimit`, `isSuccLimitRecOn_succ`, `isSuccLimitRecOn_of_isMin`
`isSuccPrelimitRecOn` 📖	CompOp	3 math math: `isSuccPrelimitRecOn_of_isSuccPrelimit`, `isSuccPrelimitRecOn_succ_of_not_isMax`, `isSuccPrelimitRecOn_succ`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isGLB_Ioi_iff_isPredPrelimit` 📖	mathematical	—	`IsGLB` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.Ioi` `IsPredPrelimit` `Preorder.toLT`	—	`isLUB_Iio_iff_isSuccPrelimit`
`isLUB_Iio_iff_isSuccPrelimit` 📖	mathematical	—	`IsLUB` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.Iio` `IsSuccPrelimit` `Preorder.toLT`	—	`LT.lt.false` `CovBy.lt` `IsLUB.unique` `isLUB_Iic` `CovBy.Iio_eq` `IsSuccPrelimit.isLUB_Iio`
`isMax_or_mem_range_pred_or_isPredLimit` 📖	mathematical	—	`IsMax` `Preorder.toLE` `PartialOrder.toPreorder` `Set` `Set.instMembership` `Set.range` `pred` `IsPredLimit`	—	`IsPredLimit.eq_1` `mem_range_pred_or_isPredPrelimit`
`isMin_or_mem_range_succ_or_isSuccLimit` 📖	mathematical	—	`IsMin` `Preorder.toLE` `PartialOrder.toPreorder` `Set` `Set.instMembership` `Set.range` `succ` `IsSuccLimit`	—	`IsSuccLimit.eq_1` `mem_range_succ_or_isSuccPrelimit`
`isPredLimitRecOn_of_isMax` 📖	mathematical	`IsMax` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`isPredLimitRecOn`	—	`isPredLimitRecOn.eq_1` `IsMax.isPredPrelimit` `isPredPrelimitRecOn_of_isPredPrelimit`
`isPredLimitRecOn_of_isPredLimit` 📖	mathematical	`IsPredLimit` `PartialOrder.toPreorder`	`isPredLimitRecOn`	—	`isPredLimitRecOn.eq_1` `IsPredLimit.isPredPrelimit` `isPredPrelimitRecOn_of_isPredPrelimit` `IsPredLimit.not_isMax`
`isPredLimitRecOn_pred` 📖	mathematical	—	`isPredLimitRecOn` `pred` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `not_isMin`	—	`isPredLimitRecOn_pred_of_not_isMin` `not_isMin`
`isPredLimitRecOn_pred_of_not_isMin` 📖	mathematical	`IsMin` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`isPredLimitRecOn` `pred`	—	`isPredLimitRecOn.eq_1` `isPredPrelimitRecOn_pred_of_not_isMin`
`isPredLimit_iff` 📖	mathematical	—	`IsPredLimit` `PartialOrder.toPreorder` `IsPredPrelimit` `Preorder.toLT`	—	`IsPredLimit.eq_1` `isMax_iff_eq_top`
`isPredLimit_toDual_iff` 📖	mathematical	—	`IsPredLimit` `OrderDual` `OrderDual.instPreorder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual` `IsSuccLimit`	—	—
`isPredPrelimitRecOn_of_isPredPrelimit` 📖	mathematical	`IsPredPrelimit` `Preorder.toLT` `PartialOrder.toPreorder`	`isPredPrelimitRecOn`	—	—
`isPredPrelimitRecOn_pred` 📖	mathematical	—	`isPredPrelimitRecOn` `pred` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `not_isMin`	—	`isPredPrelimitRecOn_pred_of_not_isMin` `not_isMin`
`isPredPrelimitRecOn_pred_of_not_isMin` 📖	mathematical	`IsMin` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`isPredPrelimitRecOn` `pred`	—	`not_isPredPrelimit_pred_of_not_isMin` `not_isPredPrelimit_iff` `isPredPrelimitRecOn.eq_1` `pred_eq_pred_iff_of_not_isMin`
`isPredPrelimit_iff` 📖	mathematical	—	`IsPredPrelimit` `Preorder.toLT` `PartialOrder.toPreorder` `IsMax` `Preorder.toLE`	—	`IsPredPrelimit.isMax` `IsMax.isPredPrelimit`
`isPredPrelimit_iff_isPredLimit` 📖	mathematical	—	`IsPredPrelimit` `Preorder.toLT` `IsPredLimit`	—	`isPredPrelimit_iff_isPredLimit_of_not_isMax` `not_isMax`
`isPredPrelimit_iff_isPredLimit_of_not_isMax` 📖	mathematical	`IsMax` `Preorder.toLE`	`IsPredPrelimit` `Preorder.toLT` `IsPredLimit`	—	`IsPredPrelimit.isPredLimit_of_not_isMax` `IsPredLimit.isPredPrelimit`
`isPredPrelimit_iff_lt_pred` 📖	mathematical	—	`IsPredPrelimit` `Preorder.toLT` `PartialOrder.toPreorder` `pred`	—	`IsPredPrelimit.lt_pred` `isPredPrelimit_of_lt_pred`
`isPredPrelimit_iff_of_noMin` 📖	mathematical	—	`IsPredPrelimit` `Preorder.toLT` `IsMax` `Preorder.toLE`	—	`IsPredPrelimit.isMax_of_noMin` `IsMax.isPredPrelimit`
`isPredPrelimit_iff_pred_ne` 📖	mathematical	—	`IsPredPrelimit` `Preorder.toLT` `PartialOrder.toPreorder`	—	`IsPredPrelimit.pred_ne` `isPredPrelimit_of_pred_ne`
`isPredPrelimit_of_lt_pred` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `pred`	`IsPredPrelimit`	—	`LT.lt.ne'` `CovBy.lt` `CovBy.pred_eq`
`isPredPrelimit_of_pred_lt` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `pred`	`IsPredPrelimit`	—	`isPredPrelimit_of_lt_pred`
`isPredPrelimit_of_pred_ne` 📖	mathematical	—	`IsPredPrelimit` `Preorder.toLT` `PartialOrder.toPreorder`	—	`CovBy.pred_eq`
`isPredPrelimit_toDual_iff` 📖	mathematical	—	`IsPredPrelimit` `OrderDual` `OrderDual.instLT` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual` `IsSuccPrelimit`	—	`OrderDual.forall` `toDual_covBy_toDual_iff`
`isPredPrelimit_top` 📖	mathematical	—	`IsPredPrelimit` `Preorder.toLT` `Top.top` `OrderTop.toTop` `Preorder.toLE`	—	`IsMax.isPredPrelimit` `isMax_top`
`isSuccLimitRecOn_of_isMin` 📖	mathematical	`IsMin` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`isSuccLimitRecOn`	—	`isSuccLimitRecOn.eq_1` `IsMin.isSuccPrelimit` `isSuccPrelimitRecOn_of_isSuccPrelimit`
`isSuccLimitRecOn_of_isSuccLimit` 📖	mathematical	`IsSuccLimit` `PartialOrder.toPreorder`	`isSuccLimitRecOn`	—	`isSuccLimitRecOn.eq_1` `IsSuccLimit.isSuccPrelimit` `isSuccPrelimitRecOn_of_isSuccPrelimit` `IsSuccLimit.not_isMin`
`isSuccLimitRecOn_succ` 📖	mathematical	—	`isSuccLimitRecOn` `succ` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `not_isMax`	—	`isSuccLimitRecOn_succ_of_not_isMax` `not_isMax`
`isSuccLimitRecOn_succ_of_not_isMax` 📖	mathematical	`IsMax` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`isSuccLimitRecOn` `succ`	—	`isSuccLimitRecOn.eq_1` `isSuccPrelimitRecOn_succ_of_not_isMax`
`isSuccLimit_iff` 📖	mathematical	—	`IsSuccLimit` `PartialOrder.toPreorder` `IsSuccPrelimit` `Preorder.toLT`	—	`IsSuccLimit.eq_1` `isMin_iff_eq_bot`
`isSuccLimit_toDual_iff` 📖	mathematical	—	`IsSuccLimit` `OrderDual` `OrderDual.instPreorder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual` `IsPredLimit`	—	—
`isSuccPrelimitRecOn_of_isSuccPrelimit` 📖	mathematical	`IsSuccPrelimit` `Preorder.toLT` `PartialOrder.toPreorder`	`isSuccPrelimitRecOn`	—	—
`isSuccPrelimitRecOn_succ` 📖	mathematical	—	`isSuccPrelimitRecOn` `succ` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `not_isMax`	—	`isSuccPrelimitRecOn_succ_of_not_isMax` `not_isMax`
`isSuccPrelimitRecOn_succ_of_not_isMax` 📖	mathematical	`IsMax` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`isSuccPrelimitRecOn` `succ`	—	`not_isSuccPrelimit_succ_of_not_isMax` `not_isSuccPrelimit_iff` `isSuccPrelimitRecOn.eq_1` `succ_eq_succ_iff_of_not_isMax`
`isSuccPrelimit_bot` 📖	mathematical	—	`IsSuccPrelimit` `Preorder.toLT` `Bot.bot` `OrderBot.toBot` `Preorder.toLE`	—	`IsMin.isSuccPrelimit` `isMin_bot`
`isSuccPrelimit_iff` 📖	mathematical	—	`IsSuccPrelimit` `Preorder.toLT` `PartialOrder.toPreorder` `IsMin` `Preorder.toLE`	—	`IsSuccPrelimit.isMin` `IsMin.isSuccPrelimit`
`isSuccPrelimit_iff_isSuccLimit` 📖	mathematical	—	`IsSuccPrelimit` `Preorder.toLT` `IsSuccLimit`	—	`isSuccPrelimit_iff_isSuccLimit_of_not_isMin` `not_isMin`
`isSuccPrelimit_iff_isSuccLimit_of_not_isMin` 📖	mathematical	`IsMin` `Preorder.toLE`	`IsSuccPrelimit` `Preorder.toLT` `IsSuccLimit`	—	`IsSuccPrelimit.isSuccLimit_of_not_isMin` `IsSuccLimit.isSuccPrelimit`
`isSuccPrelimit_iff_of_noMax` 📖	mathematical	—	`IsSuccPrelimit` `Preorder.toLT` `IsMin` `Preorder.toLE`	—	`IsSuccPrelimit.isMin_of_noMax` `IsMin.isSuccPrelimit`
`isSuccPrelimit_iff_succ_lt` 📖	mathematical	—	`IsSuccPrelimit` `Preorder.toLT` `PartialOrder.toPreorder` `succ`	—	`IsSuccPrelimit.succ_lt` `isSuccPrelimit_of_succ_lt`
`isSuccPrelimit_iff_succ_ne` 📖	mathematical	—	`IsSuccPrelimit` `Preorder.toLT` `PartialOrder.toPreorder`	—	`IsSuccPrelimit.succ_ne` `isSuccPrelimit_of_succ_ne`
`isSuccPrelimit_of_succ_lt` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `succ`	`IsSuccPrelimit`	—	`LT.lt.ne` `CovBy.lt` `CovBy.succ_eq`
`isSuccPrelimit_of_succ_ne` 📖	mathematical	—	`IsSuccPrelimit` `Preorder.toLT` `PartialOrder.toPreorder`	—	`CovBy.succ_eq`
`isSuccPrelimit_toDual_iff` 📖	mathematical	—	`IsSuccPrelimit` `OrderDual` `OrderDual.instLT` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual` `IsPredPrelimit`	—	—
`mem_range_pred_of_not_isPredPrelimit` 📖	mathematical	`IsPredPrelimit` `Preorder.toLT` `PartialOrder.toPreorder`	`Set` `Set.instMembership` `Set.range` `pred`	—	`not_isPredPrelimit_iff`
`mem_range_pred_or_isPredPrelimit` 📖	mathematical	—	`Set` `Set.instMembership` `Set.range` `pred` `PartialOrder.toPreorder` `IsPredPrelimit` `Preorder.toLT`	—	`mem_range_pred_of_not_isPredPrelimit`
`mem_range_succ_of_not_isSuccPrelimit` 📖	mathematical	`IsSuccPrelimit` `Preorder.toLT` `PartialOrder.toPreorder`	`Set` `Set.instMembership` `Set.range` `succ`	—	`not_isSuccPrelimit_iff`
`mem_range_succ_or_isSuccPrelimit` 📖	mathematical	—	`Set` `Set.instMembership` `Set.range` `succ` `PartialOrder.toPreorder` `IsSuccPrelimit` `Preorder.toLT`	—	`mem_range_succ_of_not_isSuccPrelimit`
`not_isPredLimit` 📖	mathematical	—	`IsPredLimit` `PartialOrder.toPreorder`	—	`IsPredLimit.not_isMax` `IsPredPrelimit.isMax` `IsPredLimit.isPredPrelimit`
`not_isPredLimit_iff` 📖	mathematical	—	`IsPredLimit` `IsMax` `Preorder.toLE` `IsPredPrelimit` `Preorder.toLT`	—	`IsPredLimit.eq_1` `not_and_or`
`not_isPredLimit_of_noMin` 📖	mathematical	—	`IsPredLimit`	—	`IsPredLimit.not_isMax` `IsPredPrelimit.isMax_of_noMin` `IsPredLimit.isPredPrelimit`
`not_isPredLimit_of_not_isPredPrelimit` 📖	mathematical	`IsPredPrelimit` `Preorder.toLT`	`IsPredLimit`	—	`not_isPredLimit_iff`
`not_isPredLimit_pred` 📖	mathematical	—	`IsPredLimit` `pred`	—	`IsPredLimit.pred_ne`
`not_isPredLimit_pred_of_not_isMin` 📖	mathematical	`IsMin` `Preorder.toLE`	`IsPredLimit` `pred`	—	`IsPredLimit.isMin`
`not_isPredLimit_top` 📖	mathematical	—	`IsPredLimit` `Top.top` `OrderTop.toTop` `Preorder.toLE`	—	`IsMax.not_isPredLimit` `isMax_top`
`not_isPredPrelimit` 📖	mathematical	—	`IsPredPrelimit` `Preorder.toLT` `PartialOrder.toPreorder`	—	—
`not_isPredPrelimit_iff` 📖	mathematical	—	`IsPredPrelimit` `Preorder.toLT` `PartialOrder.toPreorder` `IsMin` `Preorder.toLE` `pred`	—	`not_isPredPrelimit_iff_exists_covBy` `LT.lt.not_isMin` `CovBy.lt` `CovBy.pred_eq` `pred_covBy_of_not_isMin`
`not_isPredPrelimit_iff'` 📖	mathematical	—	`IsPredPrelimit` `Preorder.toLT` `PartialOrder.toPreorder` `Set` `Set.instMembership` `Set.range` `pred`	—	`isPredPrelimit_iff_pred_ne` `not_ne_iff` `Set.mem_range`
`not_isPredPrelimit_iff_exists_covBy` 📖	mathematical	—	`IsPredPrelimit` `CovBy`	—	—
`not_isPredPrelimit_of_noMin` 📖	mathematical	—	`IsPredPrelimit` `Preorder.toLT`	—	—
`not_isPredPrelimit_pred` 📖	mathematical	—	`IsPredPrelimit` `Preorder.toLT` `pred`	—	`IsPredPrelimit.pred_ne`
`not_isPredPrelimit_pred_of_not_isMin` 📖	mathematical	`IsMin` `Preorder.toLE`	`IsPredPrelimit` `Preorder.toLT` `pred`	—	`IsPredPrelimit.isMin`
`not_isSuccLimit` 📖	mathematical	—	`IsSuccLimit` `PartialOrder.toPreorder`	—	`IsSuccLimit.not_isMin` `IsSuccPrelimit.isMin` `IsSuccLimit.isSuccPrelimit`
`not_isSuccLimit_bot` 📖	mathematical	—	`IsSuccLimit` `Bot.bot` `OrderBot.toBot` `Preorder.toLE`	—	`IsMin.not_isSuccLimit` `isMin_bot`
`not_isSuccLimit_iff` 📖	mathematical	—	`IsSuccLimit` `IsMin` `Preorder.toLE` `IsSuccPrelimit` `Preorder.toLT`	—	`IsSuccLimit.eq_1` `not_and_or`
`not_isSuccLimit_of_noMax` 📖	mathematical	—	`IsSuccLimit`	—	`IsSuccLimit.not_isMin` `IsSuccPrelimit.isMin_of_noMax` `IsSuccLimit.isSuccPrelimit`
`not_isSuccLimit_succ` 📖	mathematical	—	`IsSuccLimit` `succ`	—	`IsSuccLimit.succ_ne`
`not_isSuccLimit_succ_of_not_isMax` 📖	mathematical	`IsMax` `Preorder.toLE`	`IsSuccLimit` `succ`	—	`IsSuccLimit.isMax`
`not_isSuccPrelimit` 📖	mathematical	—	`IsSuccPrelimit` `Preorder.toLT` `PartialOrder.toPreorder`	—	—
`not_isSuccPrelimit_iff` 📖	mathematical	—	`IsSuccPrelimit` `Preorder.toLT` `PartialOrder.toPreorder` `IsMax` `Preorder.toLE` `succ`	—	`not_isSuccPrelimit_iff_exists_covBy` `LT.lt.not_isMax` `CovBy.lt` `CovBy.succ_eq` `covBy_succ_of_not_isMax`
`not_isSuccPrelimit_iff'` 📖	mathematical	—	`IsSuccPrelimit` `Preorder.toLT` `PartialOrder.toPreorder` `Set` `Set.instMembership` `Set.range` `succ`	—	—
`not_isSuccPrelimit_iff_exists_covBy` 📖	mathematical	—	`IsSuccPrelimit` `CovBy`	—	—
`not_isSuccPrelimit_of_noMax` 📖	mathematical	—	`IsSuccPrelimit` `Preorder.toLT`	—	—
`not_isSuccPrelimit_succ` 📖	mathematical	—	`IsSuccPrelimit` `Preorder.toLT` `succ`	—	`IsSuccPrelimit.succ_ne`
`not_isSuccPrelimit_succ_of_not_isMax` 📖	mathematical	`IsMax` `Preorder.toLE`	`IsSuccPrelimit` `Preorder.toLT` `succ`	—	`IsSuccPrelimit.isMax`

Order.IsPredLimit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dual` 📖	mathematical	`Order.IsPredLimit`	`Order.IsSuccLimit` `OrderDual` `OrderDual.instPreorder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual`	—	`Order.isSuccLimit_toDual_iff`
`isGLB_Ioi` 📖	mathematical	`Order.IsPredLimit` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`IsGLB` `Preorder.toLE` `Set.Ioi`	—	`Order.IsSuccLimit.isLUB_Iio` `dual`
`isMin` 📖	mathematical	`Order.IsPredLimit` `Order.pred`	`IsMin` `Preorder.toLE`	—	`Order.IsPredPrelimit.isMin` `isPredPrelimit`
`isPredPrelimit` 📖	mathematical	`Order.IsPredLimit`	`Order.IsPredPrelimit` `Preorder.toLT`	—	—
`le_iff_forall_le` 📖	mathematical	`Order.IsPredLimit` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Preorder.toLE`	—	`Order.IsSuccLimit.le_iff_forall_le` `dual`
`lt_iff_exists_lt` 📖	mathematical	`Order.IsPredLimit` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Preorder.toLT`	—	`Order.IsSuccLimit.lt_iff_exists_lt` `dual`
`lt_pred` 📖	mathematical	`Order.IsPredLimit` `PartialOrder.toPreorder` `Preorder.toLT`	`Order.pred`	—	`Order.IsPredPrelimit.lt_pred` `isPredPrelimit`
`lt_pred_iff` 📖	mathematical	`Order.IsPredLimit` `PartialOrder.toPreorder`	`Preorder.toLT` `Order.pred`	—	`Order.IsPredPrelimit.lt_pred_iff` `isPredPrelimit`
`lt_top` 📖	mathematical	`Order.IsPredLimit` `PartialOrder.toPreorder`	`Preorder.toLT` `Top.top` `OrderTop.toTop` `Preorder.toLE`	—	`Ne.lt_top` `ne_top`
`ne_top` 📖	—	`Order.IsPredLimit`	—	—	`Order.not_isPredLimit_top`
`nonempty_Ioi` 📖	mathematical	`Order.IsPredLimit`	`Set.Nonempty` `Set.Ioi`	—	`not_isMax_iff`
`not_isMax` 📖	mathematical	`Order.IsPredLimit`	`IsMax` `Preorder.toLE`	—	—
`pred_le_iff` 📖	mathematical	`Order.IsPredLimit` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Preorder.toLE` `Order.pred`	—	`Order.IsPredPrelimit.pred_le_iff` `isPredPrelimit`
`pred_ne` 📖	—	`Order.IsPredLimit`	—	—	`Order.IsPredPrelimit.pred_ne` `isPredPrelimit`

Order.IsPredPrelimit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dual` 📖	mathematical	`Order.IsPredPrelimit`	`Order.IsSuccPrelimit` `OrderDual` `OrderDual.instLT` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual`	—	`Order.isSuccPrelimit_toDual_iff`
`isGLB_Ioi` 📖	mathematical	`Order.IsPredPrelimit` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`IsGLB` `Preorder.toLE` `Set.Ioi`	—	`Order.IsSuccPrelimit.isLUB_Iio` `dual`
`isMax` 📖	mathematical	`Order.IsPredPrelimit` `Preorder.toLT` `PartialOrder.toPreorder`	`IsMax` `Preorder.toLE`	—	`Order.IsSuccPrelimit.isMin` `instIsSuccArchimedeanOrderDual` `dual`
`isMax_of_noMin` 📖	mathematical	`Order.IsPredPrelimit` `Preorder.toLT`	`IsMax` `Preorder.toLE`	—	`Order.IsSuccPrelimit.isMin_of_noMax` `instIsSuccArchimedeanOrderDual` `OrderDual.noMaxOrder` `dual`
`isMin` 📖	mathematical	`Order.IsPredPrelimit` `Preorder.toLT` `Order.pred`	`IsMin` `Preorder.toLE`	—	`Order.pred_covBy_of_not_isMin`
`isPredLimit` 📖	mathematical	`Order.IsPredPrelimit` `Preorder.toLT`	`Order.IsPredLimit`	—	`isPredLimit_of_not_isMax` `not_isMax`
`isPredLimit_of_not_isMax` 📖	mathematical	`Order.IsPredPrelimit` `Preorder.toLT` `IsMax` `Preorder.toLE`	`Order.IsPredLimit`	—	—
`le_iff_forall_le` 📖	mathematical	`Order.IsPredPrelimit` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Preorder.toLE`	—	`Order.IsSuccPrelimit.le_iff_forall_le` `dual`
`lt_iff_exists_lt` 📖	—	`Order.IsPredPrelimit` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	—	`Order.IsSuccPrelimit.lt_iff_exists_lt` `dual`
`lt_pred` 📖	mathematical	`Order.IsPredPrelimit` `Preorder.toLT` `PartialOrder.toPreorder`	`Order.pred`	—	`IsMin.pred_eq` `lt_iff_le_and_ne'` `Order.le_pred_iff_of_not_isMin` `isMin`
`lt_pred_iff` 📖	mathematical	`Order.IsPredPrelimit` `Preorder.toLT` `PartialOrder.toPreorder`	`Order.pred`	—	`LE.le.trans_lt'` `Order.pred_le` `lt_pred`
`of_dense` 📖	mathematical	—	`Order.IsPredPrelimit`	—	`not_covBy`
`pred_le_iff` 📖	mathematical	`Order.IsPredPrelimit` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Preorder.toLE` `Order.pred`	—	`le_iff_le_iff_lt_iff_lt` `lt_pred_iff`
`pred_ne` 📖	—	`Order.IsPredPrelimit` `Preorder.toLT`	—	—	`not_isMin` `isMin`

Order.IsSuccLimit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bot_lt` 📖	mathematical	`Order.IsSuccLimit` `PartialOrder.toPreorder`	`Preorder.toLT` `Bot.bot` `OrderBot.toBot` `Preorder.toLE`	—	`Ne.bot_lt` `ne_bot`
`dual` 📖	mathematical	`Order.IsSuccLimit`	`Order.IsPredLimit` `OrderDual` `OrderDual.instPreorder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual`	—	`Order.isPredLimit_toDual_iff`
`isLUB_Iio` 📖	mathematical	`Order.IsSuccLimit` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`IsLUB` `Preorder.toLE` `Set.Iio`	—	`Order.IsSuccPrelimit.isLUB_Iio` `isSuccPrelimit`
`isMax` 📖	mathematical	`Order.IsSuccLimit` `Order.succ`	`IsMax` `Preorder.toLE`	—	`Order.IsSuccPrelimit.isMax` `isSuccPrelimit`
`isSuccPrelimit` 📖	mathematical	`Order.IsSuccLimit`	`Order.IsSuccPrelimit` `Preorder.toLT`	—	—
`le_iff_forall_le` 📖	mathematical	`Order.IsSuccLimit` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Preorder.toLE`	—	`Order.IsSuccPrelimit.le_iff_forall_le` `isSuccPrelimit`
`le_succ_iff` 📖	mathematical	`Order.IsSuccLimit` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Preorder.toLE` `Order.succ`	—	`Order.IsSuccPrelimit.le_succ_iff` `isSuccPrelimit`
`lt_iff_exists_lt` 📖	mathematical	`Order.IsSuccLimit` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Preorder.toLT`	—	`Order.IsSuccPrelimit.lt_iff_exists_lt` `isSuccPrelimit`
`ne_bot` 📖	—	`Order.IsSuccLimit`	—	—	`Order.not_isSuccLimit_bot`
`nonempty_Iio` 📖	mathematical	`Order.IsSuccLimit`	`Set.Nonempty` `Set.Iio`	—	`not_isMin_iff`
`not_isMin` 📖	mathematical	`Order.IsSuccLimit`	`IsMin` `Preorder.toLE`	—	—
`succ_lt` 📖	mathematical	`Order.IsSuccLimit` `PartialOrder.toPreorder` `Preorder.toLT`	`Order.succ`	—	`Order.IsSuccPrelimit.succ_lt` `isSuccPrelimit`
`succ_lt_iff` 📖	mathematical	`Order.IsSuccLimit` `PartialOrder.toPreorder`	`Preorder.toLT` `Order.succ`	—	`Order.IsSuccPrelimit.succ_lt_iff` `isSuccPrelimit`
`succ_ne` 📖	—	`Order.IsSuccLimit`	—	—	`Order.IsSuccPrelimit.succ_ne` `isSuccPrelimit`

Order.IsSuccPrelimit

Definitions

Name	Category	Theorems
`mid` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dual` 📖	mathematical	`Order.IsSuccPrelimit`	`Order.IsPredPrelimit` `OrderDual` `OrderDual.instLT` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual`	—	`Order.isPredPrelimit_toDual_iff`
`isLUB_Iio` 📖	mathematical	`Order.IsSuccPrelimit` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`IsLUB` `Preorder.toLE` `Set.Iio`	—	`le_of_lt` `le_of_forall_lt` `lt_iff_exists_lt` `LT.lt.trans_le`
`isMax` 📖	mathematical	`Order.IsSuccPrelimit` `Preorder.toLT` `Order.succ`	`IsMax` `Preorder.toLE`	—	`Order.covBy_succ_of_not_isMax`
`isMin` 📖	mathematical	`Order.IsSuccPrelimit` `Preorder.toLT` `PartialOrder.toPreorder`	`IsMin` `Preorder.toLE`	—	`le_rfl` `IsMax.succ_eq` `isMax`
`isMin_of_noMax` 📖	mathematical	`Order.IsSuccPrelimit` `Preorder.toLT`	`IsMin` `Preorder.toLE`	—	`LE.le.exists_succ_iterate` `le_rfl` `Order.not_isSuccPrelimit_succ` `Function.iterate_succ_apply'`
`isSuccLimit` 📖	mathematical	`Order.IsSuccPrelimit` `Preorder.toLT`	`Order.IsSuccLimit`	—	`isSuccLimit_of_not_isMin` `not_isMin`
`isSuccLimit_of_not_isMin` 📖	mathematical	`Order.IsSuccPrelimit` `Preorder.toLT` `IsMin` `Preorder.toLE`	`Order.IsSuccLimit`	—	—
`le_iff_forall_le` 📖	mathematical	`Order.IsSuccPrelimit` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Preorder.toLE`	—	`LE.le.trans` `LT.lt.le` `LE.le.not_gt`
`le_succ_iff` 📖	mathematical	`Order.IsSuccPrelimit` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Preorder.toLE` `Order.succ`	—	`le_iff_le_iff_lt_iff_lt` `succ_lt_iff`
`lt_iff_exists_lt` 📖	—	`Order.IsSuccPrelimit` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	—	`not_iff_not` `le_iff_forall_le`
`of_dense` 📖	mathematical	—	`Order.IsSuccPrelimit`	—	`not_covBy`
`succ_lt` 📖	mathematical	`Order.IsSuccPrelimit` `Preorder.toLT` `PartialOrder.toPreorder`	`Order.succ`	—	`IsMax.succ_eq` `lt_iff_le_and_ne` `Order.succ_le_iff_of_not_isMax` `isMax`
`succ_lt_iff` 📖	mathematical	`Order.IsSuccPrelimit` `Preorder.toLT` `PartialOrder.toPreorder`	`Order.succ`	—	`LE.le.trans_lt` `Order.le_succ` `succ_lt`
`succ_ne` 📖	—	`Order.IsSuccPrelimit` `Preorder.toLT`	—	—	`not_isMax` `isMax`

PredOrder

Definitions

Name	Category	Theorems
`colimitRecOn` 📖	CompOp	4 math math: `colimitRecOn_of_isPredLimit`, `colimitRecOn_pred_of_not_isMin`, `colimitRecOn_isMax`, `colimitRecOn_pred`
`prelimitRecOn` 📖	CompOp	3 math math: `prelimitRecOn_pred_of_not_isMin`, `prelimitRecOn_of_isPredPrelimit`, `prelimitRecOn_pred`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`colimitRecOn_isMax` 📖	mathematical	`IsMax` `Preorder.toLE` `PartialOrder.toPreorder`	`colimitRecOn`	—	`colimitRecOn.eq_1` `IsMax.isPredPrelimit` `prelimitRecOn_of_isPredPrelimit`
`colimitRecOn_of_isPredLimit` 📖	mathematical	`Order.IsPredLimit` `PartialOrder.toPreorder`	`colimitRecOn`	—	`colimitRecOn.eq_1` `Order.IsPredLimit.isPredPrelimit` `prelimitRecOn_of_isPredPrelimit` `Order.IsPredLimit.not_isMax`
`colimitRecOn_pred` 📖	mathematical	—	`colimitRecOn` `Order.pred` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `not_isMin`	—	`colimitRecOn_pred_of_not_isMin` `not_isMin`
`colimitRecOn_pred_of_not_isMin` 📖	mathematical	`IsMin` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`colimitRecOn` `Order.pred`	—	`colimitRecOn.eq_1` `prelimitRecOn_pred_of_not_isMin`
`prelimitRecOn_of_isPredPrelimit` 📖	mathematical	`Order.IsPredPrelimit` `Preorder.toLT` `PartialOrder.toPreorder`	`prelimitRecOn`	—	`prelimitRecOn.eq_1`
`prelimitRecOn_pred` 📖	mathematical	—	`prelimitRecOn` `Order.pred` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `not_isMin`	—	`prelimitRecOn_pred_of_not_isMin` `not_isMin`
`prelimitRecOn_pred_of_not_isMin` 📖	mathematical	`IsMin` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`prelimitRecOn` `Order.pred`	—	`Order.not_isPredPrelimit_pred_of_not_isMin` `Order.not_isPredPrelimit_iff` `prelimitRecOn.eq_1` `Order.pred_eq_pred_iff_of_not_isMin`

SuccOrder

Definitions

Name	Category	Theorems
`limitRecOn` 📖	CompOp	4 math math: `limitRecOn_succ`, `limitRecOn_succ_of_not_isMax`, `limitRecOn_of_isSuccLimit`, `limitRecOn_isMin`
`prelimitRecOn` 📖	CompOp	3 math math: `prelimitRecOn_of_isSuccPrelimit`, `prelimitRecOn_succ_of_not_isMax`, `prelimitRecOn_succ`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`limitRecOn_isMin` 📖	mathematical	`IsMin` `Preorder.toLE` `PartialOrder.toPreorder`	`limitRecOn`	—	`limitRecOn.eq_1` `IsMin.isSuccPrelimit` `prelimitRecOn_of_isSuccPrelimit`
`limitRecOn_of_isSuccLimit` 📖	mathematical	`Order.IsSuccLimit` `PartialOrder.toPreorder`	`limitRecOn`	—	`limitRecOn.eq_1` `Order.IsSuccLimit.isSuccPrelimit` `prelimitRecOn_of_isSuccPrelimit` `Order.IsSuccLimit.not_isMin`
`limitRecOn_succ` 📖	mathematical	—	`limitRecOn` `Order.succ` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `not_isMax`	—	`limitRecOn_succ_of_not_isMax` `not_isMax`
`limitRecOn_succ_of_not_isMax` 📖	mathematical	`IsMax` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`limitRecOn` `Order.succ`	—	`limitRecOn.eq_1` `prelimitRecOn_succ_of_not_isMax`
`prelimitRecOn_of_isSuccPrelimit` 📖	mathematical	`Order.IsSuccPrelimit` `Preorder.toLT` `PartialOrder.toPreorder`	`prelimitRecOn`	—	`prelimitRecOn.eq_1`
`prelimitRecOn_succ` 📖	mathematical	—	`prelimitRecOn` `Order.succ` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `not_isMax`	—	`prelimitRecOn_succ_of_not_isMax` `not_isMax`
`prelimitRecOn_succ_of_not_isMax` 📖	mathematical	`IsMax` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`prelimitRecOn` `Order.succ`	—	`Order.not_isSuccPrelimit_succ_of_not_isMax` `Order.not_isSuccPrelimit_iff` `prelimitRecOn.eq_1` `Order.succ_eq_succ_iff_of_not_isMax`

---

← Back to Index