Documentation

Mathlib.Data.PNat.Order

Order related instances for ℕ+ #

source
🔸 coverage
instance PNat.instSuccOrder :
SuccOrder ℕ+
Equations
    source
    🔸 coverage
    instance PNat.instSuccAddOrder :
    SuccAddOrder ℕ+
    Equations
      source
      📐 coverage
      instance PNat.instNoMaxOrder :
      NoMaxOrder ℕ+
      source
      📐 coverage
      @[simp]
      theorem PNat.succ_eq_add_one (n : ℕ+) :
      Order.succ n = n + 1