mathlib documentation

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.

@[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
@[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]
def enat.can_lift  :
Equations

Conversion of ℕ∞ to sending to 0.

Equations
@[simp]
theorem enat.to_nat_coe (n : ) :
@[simp]
@[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_eq_iff {m : ℕ∞} {n : } (hn : n 0) :
@[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 n P (n.succ)) (htop : ( (n : ), P n) P ) :
P a