data.enat.basic

# Definition and basic properties of extended natural numbers #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

def enat  :

Extended natural numbers ℕ∞ = with_top ℕ.

Equations
Instances for enat
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
Equations
@[protected, instance]
@[simp, norm_cast, nolint]
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]
def enat.can_lift  :
(λ (n : ℕ∞), n )
Equations
def enat.to_nat  :

Conversion of ℕ∞ to ℕ sending ∞ to 0.

Equations
@[simp]
theorem enat.to_nat_coe (n : ) :
@[simp]
theorem enat.to_nat_top  :
@[simp]
theorem enat.coe_to_nat {n : ℕ∞} :

Alias of the reverse direction of enat.coe_to_nat_eq_self.

theorem enat.to_nat_add {m n : ℕ∞} (hm : m ) (hn : n ) :
theorem enat.to_nat_sub {n : ℕ∞} (hn : n ) (m : ℕ∞) :
theorem enat.to_nat_eq_iff {m : ℕ∞} {n : } (hn : n 0) :
m = n
@[simp]
theorem enat.succ_def (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 n P (n.succ)) (htop : ( (n : ), P n) P ) :
P a