SuccPred

📁 Source: Mathlib/Data/Int/SuccPred.lean

Statistics

Metric	Count
Definitions instPredOrder, instPredSubOrder, instSuccAddOrder, instSuccOrder	4
Theorems intCast, instIsPredArchimedean, instIsSuccArchimedean, natCast_covBy, pred_eq_pred, succ_eq_succ	6
Total	10

CovBy

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
intCast 📖	—	CovBy	—	—	Int.natCast_covBy

Int

Definitions

Name	Category	Theorems
instPredOrder 📖	CompOp	2 math math: instIsPredArchimedean, pred_eq_pred
instPredSubOrder 📖	CompOp	—
instSuccAddOrder 📖	CompOp	—
instSuccOrder 📖	CompOp	2 math math: instIsSuccArchimedean, succ_eq_succ

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsPredArchimedean 📖	mathematical	—	IsPredArchimedean PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt instPredOrder	—	Order.pred_iterate sub_sub_cancel
instIsSuccArchimedean 📖	mathematical	—	IsSuccArchimedean PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt instSuccOrder	—	Order.succ_iterate add_sub_assoc add_sub_cancel_left
natCast_covBy 📖	mathematical	—	CovBy	—	Order.covBy_iff_add_one_eq instNoMaxOrderOfNontrivial IsStrictOrderedRing.toIsOrderedRing instIsStrictOrderedRing instNontrivial Nat.instNoMaxOrder
pred_eq_pred 📖	mathematical	—	Order.pred PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt instPredOrder pred	—	—
succ_eq_succ 📖	mathematical	—	Order.succ PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt instSuccOrder succ	—	—

---

← Back to Index