The positive natural numbers #
This file develops the type ℕ+
or PNat
, the subtype of natural numbers that are positive.
It is defined in Data.PNat.Defs
, but most of the development is deferred to here so
that Data.PNat.Defs
can have very few imports.
@[simp]
@[simp]
@[simp]
@[simp]
instance
PNat.covariantClass_add_le :
CovariantClass ℕ+ ℕ+ (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
instance
PNat.covariantClass_add_lt :
CovariantClass ℕ+ ℕ+ (fun x x_1 => x + x_1) fun x x_1 => x < x_1
instance
PNat.contravariantClass_add_le :
ContravariantClass ℕ+ ℕ+ (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
instance
PNat.contravariantClass_add_lt :
ContravariantClass ℕ+ ℕ+ (fun x x_1 => x + x_1) fun x x_1 => x < x_1
An equivalence between ℕ+
and ℕ
given by PNat.natPred
and Nat.succPNat
.
Instances For
The order isomorphism between ℕ and ℕ+ given by succ
.
Instances For
@[simp]
Subtraction a - b is defined in the obvious way when a > b, and by a - b = 1 if a ≤ b.
@[simp]
theorem
PNat.recOn_one
{p : ℕ+ → Sort u_1}
(p1 : p 1)
(hp : (n : ℕ+) → p n → p (n + 1))
:
PNat.recOn 1 p1 hp = p1
@[simp]
theorem
PNat.recOn_succ
(n : ℕ+)
{p : ℕ+ → Sort u_1}
(p1 : p 1)
(hp : (n : ℕ+) → p n → p (n + 1))
:
PNat.recOn (n + 1) p1 hp = hp n (PNat.recOn n p1 hp)