Documentation

Mathlib.Data.PNat.Basic

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]

theorem PNat.one_add_natPred (n : ℕ+) :

1 + PNat.natPred n = ↑n

@[simp]

theorem PNat.natPred_add_one (n : ℕ+) :

PNat.natPred n + 1 = ↑n

theorem PNat.natPred_strictMono :

StrictMono PNat.natPred

theorem PNat.natPred_monotone :

Monotone PNat.natPred

theorem PNat.natPred_injective :

Function.Injective PNat.natPred

@[simp]

theorem PNat.natPred_lt_natPred {m : ℕ+} {n : ℕ+} :

PNat.natPred m < PNat.natPred n ↔ m < n

@[simp]

theorem PNat.natPred_le_natPred {m : ℕ+} {n : ℕ+} :

PNat.natPred m ≤ PNat.natPred n ↔ m ≤ n

@[simp]

theorem PNat.natPred_inj {m : ℕ+} {n : ℕ+} :

PNat.natPred m = PNat.natPred n ↔ m = n

theorem Nat.succPNat_strictMono :

StrictMono Nat.succPNat

theorem Nat.succPNat_mono :

Monotone Nat.succPNat

@[simp]

theorem Nat.succPNat_lt_succPNat {m : ℕ} {n : ℕ} :

Nat.succPNat m < Nat.succPNat n ↔ m < n

@[simp]

theorem Nat.succPNat_le_succPNat {m : ℕ} {n : ℕ} :

Nat.succPNat m ≤ Nat.succPNat n ↔ m ≤ n

theorem Nat.succPNat_injective :

Function.Injective Nat.succPNat

@[simp]

theorem Nat.succPNat_inj {n : ℕ} {m : ℕ} :

Nat.succPNat n = Nat.succPNat m ↔ n = m

@[simp]

theorem PNat.coe_inj {m : ℕ+} {n : ℕ+} :

↑m = ↑n ↔ m = n

We now define a long list of structures on ℕ+ induced by similar structures on ℕ. Most of these behave in a completely obvious way, but there are a few things to be said about subtraction, division and powers.

@[simp]

theorem PNat.add_coe (m : ℕ+) (n : ℕ+) :

↑(m + n) = ↑m + ↑n

def PNat.coeAddHom :

AddHom ℕ+ ℕ

coe promoted to an AddHom, that is, a morphism which preserves addition.

Equations

PNat.coeAddHom = { toFun := Coe.coe, map_add' := PNat.add_coe }

instance PNat.covariantClass_add_le :

CovariantClass ℕ+ ℕ+ (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

Equations

PNat.covariantClass_add_le = PNat.covariantClass_add_le.proof_1

instance PNat.covariantClass_add_lt :

CovariantClass ℕ+ ℕ+ (fun x x_1 => x + x_1) fun x x_1 => x < x_1

Equations

PNat.covariantClass_add_lt = PNat.covariantClass_add_lt.proof_1

instance PNat.contravariantClass_add_le :

ContravariantClass ℕ+ ℕ+ (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

Equations

PNat.contravariantClass_add_le = PNat.contravariantClass_add_le.proof_1

instance PNat.contravariantClass_add_lt :

ContravariantClass ℕ+ ℕ+ (fun x x_1 => x + x_1) fun x x_1 => x < x_1

Equations

PNat.contravariantClass_add_lt = PNat.contravariantClass_add_lt.proof_1

@[simp]

theorem Equiv.pnatEquivNat_apply :

↑Equiv.pnatEquivNat = PNat.natPred

@[simp]

theorem Equiv.pnatEquivNat_symm_apply :

↑(Equiv.symm Equiv.pnatEquivNat) = Nat.succPNat

def Equiv.pnatEquivNat :

An equivalence between ℕ+ and ℕ given by PNat.natPred and Nat.succPNat.

Equations

Equiv.pnatEquivNat = { toFun := PNat.natPred, invFun := Nat.succPNat, left_inv := PNat.succPNat_natPred, right_inv := Nat.natPred_succPNat }

@[simp]

theorem OrderIso.pnatIsoNat_apply :

↑(RelIso.toRelEmbedding OrderIso.pnatIsoNat).toEmbedding = PNat.natPred

def OrderIso.pnatIsoNat :

The order isomorphism between ℕ and ℕ+ given by succ.

Equations

OrderIso.pnatIsoNat = { toEquiv := Equiv.pnatEquivNat, map_rel_iff' := @OrderIso.pnatIsoNat.proof_1 }

@[simp]

theorem OrderIso.pnatIsoNat_symm_apply :

↑(RelIso.toRelEmbedding (OrderIso.symm OrderIso.pnatIsoNat)).toEmbedding = Nat.succPNat

theorem PNat.lt_add_one_iff {a : ℕ+} {b : ℕ+} :

a < b + 1 ↔ a ≤ b

theorem PNat.add_one_le_iff {a : ℕ+} {b : ℕ+} :

a + 1 ≤ b ↔ a < b

instance PNat.instOrderBotPNatToLEToPreorderToPartialOrderToOrderedCancelCommMonoidInstPNatLinearOrderedCancelCommMonoid :

Equations

One or more equations did not get rendered due to their size.

@[simp]

theorem PNat.bot_eq_one :

@[simp]

theorem PNat.mk_bit0 (n : ℕ) {h : 0 < bit0 n} :

{ val := bit0 n, property := h } = bit0 { val := n, property := (_ : 0 < n) }

@[simp]

theorem PNat.mk_bit1 (n : ℕ) {h : 0 < bit1 n} {k : 0 < n} :

{ val := bit1 n, property := h } = bit1 { val := n, property := k }

@[simp]

theorem PNat.bit0_le_bit0 (n : ℕ+) (m : ℕ+) :

bit0 n ≤ bit0 m ↔ bit0 ↑n ≤ bit0 ↑m

@[simp]

theorem PNat.bit0_le_bit1 (n : ℕ+) (m : ℕ+) :

bit0 n ≤ bit1 m ↔ bit0 ↑n ≤ bit1 ↑m

@[simp]

theorem PNat.bit1_le_bit0 (n : ℕ+) (m : ℕ+) :

bit1 n ≤ bit0 m ↔ bit1 ↑n ≤ bit0 ↑m

@[simp]

theorem PNat.bit1_le_bit1 (n : ℕ+) (m : ℕ+) :

bit1 n ≤ bit1 m ↔ bit1 ↑n ≤ bit1 ↑m

@[simp]

theorem PNat.mul_coe (m : ℕ+) (n : ℕ+) :

↑(m * n) = ↑m * ↑n

def PNat.coeMonoidHom :

PNat.coe promoted to a MonoidHom.

Equations

PNat.coeMonoidHom = { toOneHom := { toFun := Coe.coe, map_one' := PNat.one_coe }, map_mul' := PNat.mul_coe }

@[simp]

theorem PNat.coe_coeMonoidHom :

↑PNat.coeMonoidHom = Coe.coe

@[simp]

theorem PNat.le_one_iff {n : ℕ+} :

n ≤ 1 ↔ n = 1

theorem PNat.lt_add_left (n : ℕ+) (m : ℕ+) :

n < m + n

theorem PNat.lt_add_right (n : ℕ+) (m : ℕ+) :

n < n + m

@[simp]

theorem PNat.coe_bit0 (a : ℕ+) :

↑(bit0 a) = bit0 ↑a

@[simp]

theorem PNat.coe_bit1 (a : ℕ+) :

↑(bit1 a) = bit1 ↑a

@[simp]

theorem PNat.pow_coe (m : ℕ+) (n : ℕ) :

↑(Pow.pow m n) = ↑m ^ n

instance PNat.instSubPNat :

Subtraction a - b is defined in the obvious way when a > b, and by a - b = 1 if a ≤ b.

Equations

PNat.instSubPNat = { sub := fun a b => Nat.toPNat' (↑a - ↑b) }

theorem PNat.sub_coe (a : ℕ+) (b : ℕ+) :

↑(a - b) = if b < a then ↑a - ↑b else 1

theorem PNat.add_sub_of_lt {a : ℕ+} {b : ℕ+} :

a < b → a + (b - a) = b

theorem PNat.exists_eq_succ_of_ne_one {n : ℕ+} :

n ≠ 1 → ∃ k, n = k + 1

If n : ℕ+ is different from 1, then it is the successor of some k : ℕ+.

def PNat.caseStrongInductionOn {p : ℕ+ → Sort u_1} (a : ℕ+) (hz : p 1) (hi : (n : ℕ+) → ((m : ℕ+) → m ≤ n → p m) → p (n + 1)) :

p a

Strong induction on ℕ+, with n = 1 treated separately.

Equations

One or more equations did not get rendered due to their size.

def PNat.recOn (n : ℕ+) {p : ℕ+ → Sort u_1} (p1 : p 1) (hp : (n : ℕ+) → p n → p (n + 1)) :

p n

An induction principle for ℕ+: it takes values in Sort*, so it applies also to Types, not only to Prop.

Equations

One or more equations did not get rendered due to their size.

@[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)

theorem PNat.modDivAux_spec (k : ℕ+) (r : ℕ) (q : ℕ) :

¬(r = 0 ∧ q = 0) → ↑(PNat.modDivAux k r q).fst + ↑k * (PNat.modDivAux k r q).snd = r + ↑k * q

theorem PNat.mod_add_div (m : ℕ+) (k : ℕ+) :

↑(PNat.mod m k) + ↑k * PNat.div m k = ↑m

theorem PNat.div_add_mod (m : ℕ+) (k : ℕ+) :

↑k * PNat.div m k + ↑(PNat.mod m k) = ↑m

theorem PNat.mod_add_div' (m : ℕ+) (k : ℕ+) :

↑(PNat.mod m k) + PNat.div m k * ↑k = ↑m

theorem PNat.div_add_mod' (m : ℕ+) (k : ℕ+) :

PNat.div m k * ↑k + ↑(PNat.mod m k) = ↑m

theorem PNat.mod_le (m : ℕ+) (k : ℕ+) :

PNat.mod m k ≤ m ∧ PNat.mod m k ≤ k

theorem PNat.dvd_iff {k : ℕ+} {m : ℕ+} :

k ∣ m ↔ ↑k ∣ ↑m

theorem PNat.dvd_iff' {k : ℕ+} {m : ℕ+} :

k ∣ m ↔ PNat.mod m k = k

theorem PNat.le_of_dvd {m : ℕ+} {n : ℕ+} :

m ∣ n → m ≤ n

theorem PNat.mul_div_exact {m : ℕ+} {k : ℕ+} (h : k ∣ m) :

k * PNat.divExact m k = m

theorem PNat.dvd_antisymm {m : ℕ+} {n : ℕ+} :

m ∣ n → n ∣ m → m = n

theorem PNat.dvd_one_iff (n : ℕ+) :

n ∣ 1 ↔ n = 1

theorem PNat.pos_of_div_pos {n : ℕ+} {a : ℕ} (h : a ∣ ↑n) :

0 < a