mathlib documentation

data.nat.enat

Definition and basic properties of extended natural numbers #

In this file we define enat (notation: ℕ∞) to be with_top and prove some basic lemmas about this type.

@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
noncomputable def enat.has_bot  :
@[protected, instance]
Equations
@[simp, norm_cast]
theorem enat.coe_zero  :
0 = 0
@[simp, norm_cast]
theorem enat.coe_one  :
1 = 1
@[simp, norm_cast]
theorem enat.coe_add (m n : ) :
(m + n) = m + n
@[simp, norm_cast]
theorem enat.coe_sub (m n : ) :
(m - n) = m - n
@[simp, norm_cast]
theorem enat.coe_mul (m n : ) :
(m * n) = m * n
@[protected, instance]
Equations

Conversion of ℕ∞ to sending to 0.

Equations
@[simp]
theorem enat.succ_def (m : ℕ∞) :
order.succ m = m + 1
theorem enat.add_one_le_of_lt {m n : ℕ∞} (h : m < n) :
m + 1 n
theorem enat.add_one_le_iff {m n : ℕ∞} (hm : m ) :
m + 1 n m < n
theorem enat.one_le_iff_pos {n : ℕ∞} :
1 n 0 < n
theorem enat.one_le_iff_ne_zero {n : ℕ∞} :
1 n n 0
theorem enat.le_of_lt_add_one {m n : ℕ∞} (h : m < n + 1) :
m n
theorem enat.nat_induction {P : ℕ∞ → Prop} (a : ℕ∞) (h0 : P 0) (hsuc : ∀ (n : ), P nP (n.succ)) (htop : (∀ (n : ), P n)P ) :
P a