Order

📁 Source: Mathlib/Data/PNat/Order.lean

Statistics

Metric	Count
Definitions instSuccAddOrder, instSuccOrder	2
Theorems instNoMaxOrder, succ_eq_add_one	2
Total	4

PNat

Definitions

Name	Category	Theorems
instSuccAddOrder 📖	CompOp	—
instSuccOrder 📖	CompOp	1 math math: succ_eq_add_one

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instNoMaxOrder 📖	mathematical	—	NoMaxOrder PNat Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderPNat	—	lt_succ_self
succ_eq_add_one 📖	mathematical	—	Order.succ PNat PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderPNat instSuccOrder instAddPNat instOfNatPNatOfNeZeroNat	—	—

---

← Back to Index