SuccPred

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

Statistics

Metric	Count
Definitions `PredSubOrder`, `toPredOrder`, `SuccAddOrder`, `toSuccOrder`	4
Theorems `lt_sub_natCast`, `lt_sub_one`, `lt_sub_natCast`, `lt_sub_one`, `add_natCast_lt`, `add_one_lt`, `natCast_lt`, `add_natCast_lt`, `add_one_lt`, `add_one_le_iff`, `add_one_le_iff_of_not_isMax`, `add_one_le_of_lt`, `covBy_add_one`, `covBy_iff_add_one_eq`, `covBy_iff_sub_one_eq`, `le_of_lt_add_one`, `le_of_sub_one_lt`, `le_sub_one_iff`, `le_sub_one_iff_of_not_isMin`, `le_sub_one_of_lt`, `lt_add_one_iff`, `lt_add_one_iff_of_not_isMax`, `lt_one_iff_nonpos`, `not_isMax_zero`, `not_isSuccLimit_natCast`, `one_le_iff_pos`, `pred_eq_sub_one`, `pred_iterate`, `sub_one_covBy`, `sub_one_lt_iff`, `sub_one_lt_iff_of_not_isMin`, `sub_one_wcovBy`, `succ_eq_add_one`, `succ_eq_zero`, `succ_iterate`, `wcovBy_add_one`, `pred_eq_sub_one`, `succ_eq_add_one`, `antitoneOn_of_add_one_le`, `antitoneOn_of_le_sub_one`, `antitone_of_add_one_le`, `antitone_of_le_sub_one`, `monotoneOn_of_le_add_one`, `monotoneOn_of_sub_one_le`, `monotone_of_le_add_one`, `monotone_of_sub_one_le`, `strictAntiOn_of_add_one_lt`, `strictAntiOn_of_lt_sub_one`, `strictAnti_of_add_one_lt`, `strictAnti_of_lt_sub_one`, `strictMonoOn_of_lt_add_one`, `strictMonoOn_of_sub_one_lt`, `strictMono_of_lt_add_one`, `strictMono_of_sub_one_lt`	54
Total	58

Order

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_one_le_iff` 📖	mathematical	—	`Preorder.toLE` `Preorder.toLT`	—	`add_one_le_iff_of_not_isMax` `not_isMax`
`add_one_le_iff_of_not_isMax` 📖	mathematical	`IsMax` `Preorder.toLE`	`Preorder.toLT`	—	`succ_eq_add_one` `succ_le_iff_of_not_isMax`
`add_one_le_of_lt` 📖	mathematical	`Preorder.toLT`	`Preorder.toLE`	—	`succ_eq_add_one` `succ_le_of_lt`
`covBy_add_one` 📖	mathematical	—	`CovBy` `Preorder.toLT`	—	`succ_eq_add_one` `covBy_succ`
`covBy_iff_add_one_eq` 📖	mathematical	—	`CovBy` `Preorder.toLT` `PartialOrder.toPreorder`	—	`succ_eq_add_one` `succ_eq_iff_covBy`
`covBy_iff_sub_one_eq` 📖	mathematical	—	`CovBy` `Preorder.toLT` `PartialOrder.toPreorder`	—	`pred_eq_sub_one` `pred_eq_iff_covBy`
`le_of_lt_add_one` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Preorder.toLE`	—	`le_of_lt_succ` `succ_eq_add_one`
`le_of_sub_one_lt` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Preorder.toLE`	—	`le_of_pred_lt` `pred_eq_sub_one`
`le_sub_one_iff` 📖	mathematical	—	`Preorder.toLE` `Preorder.toLT`	—	`le_sub_one_iff_of_not_isMin` `not_isMin`
`le_sub_one_iff_of_not_isMin` 📖	mathematical	`IsMin` `Preorder.toLE`	`Preorder.toLT`	—	`pred_eq_sub_one` `le_pred_iff_of_not_isMin`
`le_sub_one_of_lt` 📖	mathematical	`Preorder.toLT`	`Preorder.toLE`	—	`pred_eq_sub_one` `le_pred_of_lt`
`lt_add_one_iff` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Preorder.toLE`	—	`lt_add_one_iff_of_not_isMax` `not_isMax`
`lt_add_one_iff_of_not_isMax` 📖	mathematical	`IsMax` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Preorder.toLT`	—	`succ_eq_add_one` `lt_succ_iff_of_not_isMax`
`lt_one_iff_nonpos` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddMonoidWithOne.toOne` `Preorder.toLE` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid`	—	`lt_succ_iff_of_not_isMax` `not_isMax_zero` `succ_eq_add_one` `zero_add`
`not_isMax_zero` 📖	mathematical	—	`IsMax` `Preorder.toLE` `PartialOrder.toPreorder`	—	`not_isMax_iff` `one_pos`
`not_isSuccLimit_natCast` 📖	mathematical	—	`IsSuccLimit` `PartialOrder.toPreorder` `AddMonoidWithOne.toNatCast`	—	`LT.lt.false` `IsSuccLimit.natCast_lt`
`one_le_iff_pos` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `AddMonoidWithOne.toOne` `Preorder.toLT` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid`	—	`succ_le_iff_of_not_isMax` `not_isMax_zero` `succ_eq_add_one` `zero_add`
`pred_eq_sub_one` 📖	mathematical	—	`pred` `PredSubOrder.toPredOrder`	—	`PredSubOrder.pred_eq_sub_one`
`pred_iterate` 📖	mathematical	—	`Nat.iterate` `pred` `PredSubOrder.toPredOrder` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `AddCommGroupWithOne.toAddGroupWithOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `AddMonoidWithOne.toNatCast`	—	`Function.iterate_zero_apply` `Nat.cast_zero` `sub_zero` `Function.iterate_succ_apply'` `Nat.cast_add` `pred_eq_sub_one` `Nat.cast_one` `sub_sub`
`sub_one_covBy` 📖	mathematical	—	`CovBy` `Preorder.toLT`	—	`pred_eq_sub_one` `pred_covBy`
`sub_one_lt_iff` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Preorder.toLE`	—	`sub_one_lt_iff_of_not_isMin` `not_isMin`
`sub_one_lt_iff_of_not_isMin` 📖	mathematical	`IsMin` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Preorder.toLT`	—	`pred_eq_sub_one` `pred_lt_iff_of_not_isMin`
`sub_one_wcovBy` 📖	mathematical	—	`WCovBy`	—	`pred_eq_sub_one` `pred_wcovBy`
`succ_eq_add_one` 📖	mathematical	—	`succ` `SuccAddOrder.toSuccOrder`	—	`SuccAddOrder.succ_eq_add_one`
`succ_eq_zero` 📖	mathematical	—	`WithBot.succ` `PartialOrder.toPreorder` `SuccAddOrder.toSuccOrder` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddZero.toZero` `Bot.bot` `WithBot` `WithBot.bot`	—	`bot_eq_zero` `max_of_succ_le`
`succ_iterate` 📖	mathematical	—	`Nat.iterate` `succ` `SuccAddOrder.toSuccOrder` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `AddMonoidWithOne.toAddMonoid` `AddMonoidWithOne.toOne` `AddMonoidWithOne.toNatCast`	—	`Function.iterate_zero_apply` `Nat.cast_zero` `add_zero` `Function.iterate_succ_apply'` `Nat.cast_add` `succ_eq_add_one` `Nat.cast_one` `add_assoc`
`wcovBy_add_one` 📖	mathematical	—	`WCovBy`	—	`succ_eq_add_one` `wcovBy_succ`

Order.IsPredLimit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`lt_sub_natCast` 📖	mathematical	`Order.IsPredLimit` `PartialOrder.toPreorder` `Preorder.toLT`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `AddCommGroupWithOne.toAddGroupWithOne` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne`	—	`Order.IsPredPrelimit.lt_sub_natCast` `isPredPrelimit`
`lt_sub_one` 📖	—	`Order.IsPredLimit` `PartialOrder.toPreorder` `Preorder.toLT`	—	—	`Order.IsPredPrelimit.lt_sub_one` `isPredPrelimit`

Order.IsPredPrelimit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`lt_sub_natCast` 📖	mathematical	`Order.IsPredPrelimit` `Preorder.toLT` `PartialOrder.toPreorder`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `AddCommGroupWithOne.toAddGroupWithOne` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne`	—	`Nat.cast_zero` `sub_zero` `Nat.cast_add_one` `sub_sub` `lt_sub_one`
`lt_sub_one` 📖	—	`Order.IsPredPrelimit` `Preorder.toLT` `PartialOrder.toPreorder`	—	—	`Order.pred_eq_sub_one` `lt_pred`

Order.IsSuccLimit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_natCast_lt` 📖	mathematical	`Order.IsSuccLimit` `PartialOrder.toPreorder` `Preorder.toLT`	`AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `AddMonoidWithOne.toAddMonoid` `AddMonoidWithOne.toNatCast`	—	`Order.IsSuccPrelimit.add_natCast_lt` `isSuccPrelimit`
`add_one_lt` 📖	—	`Order.IsSuccLimit` `PartialOrder.toPreorder` `Preorder.toLT`	—	—	`Order.IsSuccPrelimit.add_one_lt` `isSuccPrelimit`
`natCast_lt` 📖	mathematical	`Order.IsSuccLimit` `PartialOrder.toPreorder`	`Preorder.toLT` `AddMonoidWithOne.toNatCast`	—	`bot_eq_zero` `zero_add` `add_natCast_lt` `bot_lt`

Order.IsSuccPrelimit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_natCast_lt` 📖	mathematical	`Order.IsSuccPrelimit` `Preorder.toLT` `PartialOrder.toPreorder`	`AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `AddMonoidWithOne.toAddMonoid` `AddMonoidWithOne.toNatCast`	—	`Nat.cast_zero` `add_zero` `Nat.cast_add_one` `add_assoc` `add_one_lt`
`add_one_lt` 📖	—	`Order.IsSuccPrelimit` `Preorder.toLT` `PartialOrder.toPreorder`	—	—	`Order.succ_eq_add_one` `succ_lt`

PredSubOrder

Definitions

Name	Category	Theorems
`toPredOrder` 📖	CompOp	3 math math: `Order.pred_iterate`, `pred_eq_sub_one`, `Order.pred_eq_sub_one`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`pred_eq_sub_one` 📖	mathematical	—	`PredOrder.pred` `toPredOrder`	—	—

SuccAddOrder

Definitions

Name	Category	Theorems
`toSuccOrder` 📖	CompOp	8 math math: `Order.succ_eq_add_one`, `Order.succ_eq_zero`, `Order.succ_iterate`, `WithBot.succ_one`, `WithBot.succ_zero`, `WithBot.succ_natCast`, `succ_eq_add_one`, `WithBot.succ_ofNat`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`succ_eq_add_one` 📖	mathematical	—	`SuccOrder.succ` `toSuccOrder`	—	—

(root)

Definitions

Name	Category	Theorems
`PredSubOrder` 📖	CompData	—
`SuccAddOrder` 📖	CompData	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`antitoneOn_of_add_one_le` 📖	mathematical	`Preorder.toLE`	`AntitoneOn` `PartialOrder.toPreorder`	—	`Order.succ_eq_add_one` `antitoneOn_of_succ_le`
`antitoneOn_of_le_sub_one` 📖	mathematical	`Preorder.toLE`	`AntitoneOn` `PartialOrder.toPreorder`	—	`Order.pred_eq_sub_one` `antitoneOn_of_le_pred`
`antitone_of_add_one_le` 📖	mathematical	`Preorder.toLE`	`Antitone` `PartialOrder.toPreorder`	—	`Order.succ_eq_add_one` `antitone_of_succ_le`
`antitone_of_le_sub_one` 📖	mathematical	`Preorder.toLE`	`Antitone` `PartialOrder.toPreorder`	—	`Order.pred_eq_sub_one` `antitone_of_le_pred`
`monotoneOn_of_le_add_one` 📖	mathematical	`Preorder.toLE`	`MonotoneOn` `PartialOrder.toPreorder`	—	`Order.succ_eq_add_one` `monotoneOn_of_le_succ`
`monotoneOn_of_sub_one_le` 📖	mathematical	`Preorder.toLE`	`MonotoneOn` `PartialOrder.toPreorder`	—	`Order.pred_eq_sub_one` `monotoneOn_of_pred_le`
`monotone_of_le_add_one` 📖	mathematical	`Preorder.toLE`	`Monotone` `PartialOrder.toPreorder`	—	`Order.succ_eq_add_one` `monotone_of_le_succ`
`monotone_of_sub_one_le` 📖	mathematical	`Preorder.toLE`	`Monotone` `PartialOrder.toPreorder`	—	`Order.pred_eq_sub_one` `monotone_of_pred_le`
`strictAntiOn_of_add_one_lt` 📖	mathematical	`Preorder.toLT`	`StrictAntiOn` `PartialOrder.toPreorder`	—	`Order.succ_eq_add_one` `strictAntiOn_of_succ_lt`
`strictAntiOn_of_lt_sub_one` 📖	mathematical	`Preorder.toLT`	`StrictAntiOn` `PartialOrder.toPreorder`	—	`Order.pred_eq_sub_one` `strictAntiOn_of_lt_pred`
`strictAnti_of_add_one_lt` 📖	mathematical	`Preorder.toLT`	`StrictAnti` `PartialOrder.toPreorder`	—	`Order.succ_eq_add_one` `strictAnti_of_succ_lt`
`strictAnti_of_lt_sub_one` 📖	mathematical	`Preorder.toLT`	`StrictAnti` `PartialOrder.toPreorder`	—	`Order.pred_eq_sub_one` `strictAnti_of_lt_pred`
`strictMonoOn_of_lt_add_one` 📖	mathematical	`Preorder.toLT`	`StrictMonoOn` `PartialOrder.toPreorder`	—	`Order.succ_eq_add_one` `strictMonoOn_of_lt_succ`
`strictMonoOn_of_sub_one_lt` 📖	mathematical	`Preorder.toLT`	`StrictMonoOn` `PartialOrder.toPreorder`	—	`Order.pred_eq_sub_one` `strictMonoOn_of_pred_lt`
`strictMono_of_lt_add_one` 📖	mathematical	`Preorder.toLT`	`StrictMono` `PartialOrder.toPreorder`	—	`Order.succ_eq_add_one` `strictMono_of_lt_succ`
`strictMono_of_sub_one_lt` 📖	mathematical	`Preorder.toLT`	`StrictMono` `PartialOrder.toPreorder`	—	`Order.pred_eq_sub_one` `strictMono_of_pred_lt`

---

← Back to Index