data.pnat.basic - mathlib3 docs

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.

source

@[simp, norm_cast]

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

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

source

def pnat.coe_add_hom :

add_hom ℕ+ ℕ

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

Equations

pnat.coe_add_hom = {to_fun := coe coe_to_lift, map_add' := pnat.add_coe}

source

@[protected, instance]

def pnat.has_le.le.covariant_class :

covariant_class ℕ+ ℕ+ has_add.add has_le.le

source

@[protected, instance]

def pnat.has_lt.lt.covariant_class :

covariant_class ℕ+ ℕ+ has_add.add has_lt.lt

source

@[protected, instance]

def pnat.has_le.le.contravariant_class :

contravariant_class ℕ+ ℕ+ has_add.add has_le.le

source

@[protected, instance]

def pnat.has_lt.lt.contravariant_class :

contravariant_class ℕ+ ℕ+ has_add.add has_lt.lt

source

@[simp]

theorem equiv.pnat_equiv_nat_symm_apply :

⇑(equiv.pnat_equiv_nat.symm) = nat.succ_pnat

source

def equiv.pnat_equiv_nat :

ℕ+ ≃ ℕ

An equivalence between ℕ+ and ℕ given by pnat.nat_pred and nat.succ_pnat.

Equations

equiv.pnat_equiv_nat = {to_fun := pnat.nat_pred, inv_fun := nat.succ_pnat, left_inv := pnat.succ_pnat_nat_pred, right_inv := nat.nat_pred_succ_pnat}

source

@[simp]

theorem equiv.pnat_equiv_nat_apply :

⇑equiv.pnat_equiv_nat = pnat.nat_pred

source

def order_iso.pnat_iso_nat :

ℕ+ ≃o ℕ

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

Equations

order_iso.pnat_iso_nat = {to_equiv := equiv.pnat_equiv_nat, map_rel_iff' := order_iso.pnat_iso_nat._proof_1}

source

@[simp]

theorem order_iso.pnat_iso_nat_apply :

⇑order_iso.pnat_iso_nat = pnat.nat_pred

source

@[simp]

theorem order_iso.pnat_iso_nat_symm_apply :

⇑(order_iso.pnat_iso_nat.symm) = nat.succ_pnat

source

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

a < b + 1 ↔ a ≤ b

source

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

a + 1 ≤ b ↔ a < b

source

@[protected, instance]

def pnat.order_bot :

order_bot ℕ+

Equations

pnat.order_bot = {bot := 1, bot_le := pnat.order_bot._proof_1}

source

@[simp]

theorem pnat.bot_eq_one :

⊥ = 1

source

@[simp]

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

⟨bit0 n, h⟩ = bit0 ⟨n, _⟩

source

@[simp]

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

⟨bit1 n, h⟩ = bit1 ⟨n, k⟩

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp, norm_cast]

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

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

source

def pnat.coe_monoid_hom :

ℕ+ →* ℕ

pnat.coe promoted to a monoid_hom.

Equations

pnat.coe_monoid_hom = {to_fun := coe coe_to_lift, map_one' := pnat.one_coe, map_mul' := pnat.mul_coe}

source

@[simp]

theorem pnat.coe_coe_monoid_hom :

⇑pnat.coe_monoid_hom = coe

source

@[simp]

theorem pnat.le_one_iff {n : ℕ+} :

n ≤ 1 ↔ n = 1

source

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

n < m + n

source

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

n < n + m

source

@[simp, norm_cast]

theorem pnat.coe_bit0 (a : ℕ+) :

↑(bit0 a) = bit0 ↑a

source

@[simp, norm_cast]

theorem pnat.coe_bit1 (a : ℕ+) :

↑(bit1 a) = bit1 ↑a

source

@[simp, norm_cast]

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

↑(m ^ n) = ↑m ^ n

source

@[protected, instance]

def pnat.has_sub :

has_sub ℕ+

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

Equations

pnat.has_sub = {sub := λ (a b : ℕ+), (↑a - ↑b).to_pnat'}

source

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

↑(a - b) = ite (b < a) (↑a - ↑b) 1

source

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

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

source

theorem pnat.exists_eq_succ_of_ne_one {n : ℕ+} (h1 : n ≠ 1) :

∃ (k : ℕ+), n = k + 1

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

source

def pnat.case_strong_induction_on {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

a.case_strong_induction_on hz hi = a.strong_induction_on (λ (k : ℕ+) (hk : Π (m : ℕ+), m < k → p m), subtype.cases_on k (λ (k : ℕ) (kprop : 0 < k) (hk : Π (m : ℕ+), m < ⟨k, kprop⟩ → p m), k.cases_on (λ (kprop : 0 < 0) (hk : Π (m : ℕ+), m < ⟨0, kprop⟩ → p m), _.elim) (λ (k : ℕ) (kprop : 0 < k.succ) (hk : Π (m : ℕ+), m < ⟨k.succ, kprop⟩ → p m), k.cases_on (λ (kprop : 0 < 1) (hk : Π (m : ℕ+), m < ⟨1, kprop⟩ → p m), hz) (λ (k : ℕ) (kprop : 0 < k.succ.succ) (hk : Π (m : ℕ+), m < ⟨k.succ.succ, kprop⟩ → p m), hi ⟨k.succ, _⟩ (λ (m : ℕ+) (hm : m ≤ ⟨k.succ, _⟩), hk m _)) kprop hk) kprop hk) hk)

source

def pnat.rec_on (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

n.rec_on p1 hp = subtype.cases_on n (λ (n : ℕ) (h : 0 < n), nat.rec (λ (h : 0 < 0), absurd h pnat.rec_on._proof_1) (λ (n : ℕ) (IH : Π (h : 0 < n), p ⟨n, h⟩) (h : 0 < n.succ), n.cases_on (λ (IH : Π (h : 0 < 0), p ⟨0, h⟩) (h : 0 < 1), p1) (λ (n : ℕ) (IH : Π (h : 0 < n.succ), p ⟨n.succ, h⟩) (h : 0 < n.succ.succ), hp ⟨n.succ, _⟩ (IH _)) IH h) n h)