# Definition and basic properties of extended natural numbers #

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

## Implementation details #

There are two natural coercions from ℕ to WithTop ℕ = ENat: WithTop.some and Nat.cast. In Lean 3, this difference was hidden in typeclass instances. Since these instances were definitionally equal, we did not duplicate generic lemmas about WithTop α and WithTop.some coercion for ENat and Nat.cast coercion. If you need to apply a lemma about WithTop, you may either rewrite back and forth using ENat.some_eq_coe, or restate the lemma for ENat.

Equations
Equations
Equations
Equations
Equations
Equations
instance ENat.instIsWellOrderLt :
IsWellOrder ℕ∞ fun (x1 x2 : ℕ∞) => x1 < x2
Equations
@[simp]
theorem ENat.some_eq_coe :
WithTop.some = Nat.cast

Lemmas about WithTop expect (and can output) WithTop.some but the normal form for coercion ℕ → ℕ∞ is Nat.cast.

theorem ENat.coe_zero :
0 = 0
theorem ENat.coe_one :
1 = 1
theorem ENat.coe_add (m : ) (n : ) :
(m + n) = m + n
@[simp]
theorem ENat.coe_sub (m : ) (n : ) :
(m - n) = m - n
@[simp]
theorem ENat.coe_mul (m : ) (n : ) :
(m * n) = m * n
@[simp]
theorem ENat.mul_top {m : ℕ∞} (hm : m 0) :
@[simp]
theorem ENat.top_mul {m : ℕ∞} (hm : m 0) :
theorem ENat.top_pow {n : } (n_pos : 0 < n) :
instance ENat.canLift :
CanLift ℕ∞ Nat.cast fun (x : ℕ∞) => x
Equations
Equations

Conversion of ℕ∞ to ℕ sending ∞ to 0.

Equations
Instances For

Homomorphism from ℕ∞ to ℕ sending ∞ to 0.

Equations
Instances For
@[simp]
theorem ENat.toNatHom_apply (n : ) :
ENat.toNatHom n = (↑n).toNat
@[simp]
theorem ENat.toNat_coe (n : ) :
(↑n).toNat = n
@[simp]
theorem ENat.toNat_zero :
= 0
@[simp]
theorem ENat.toNat_one :
= 1
@[simp]
theorem ENat.toNat_ofNat (n : ) [n.AtLeastTwo] :
(OfNat.ofNat n).toNat = n
@[simp]
theorem ENat.toNat_top :
.toNat = 0
@[simp]
theorem ENat.toNat_eq_zero {n : ℕ∞} :
n.toNat = 0 n = 0 n =
@[simp]
theorem ENat.recTopCoe_zero {C : ℕ∞Sort u_1} (d : C ) (f : (a : ) → C a) :
= f 0
@[simp]
theorem ENat.recTopCoe_one {C : ℕ∞Sort u_1} (d : C ) (f : (a : ) → C a) :
= f 1
@[simp]
theorem ENat.recTopCoe_ofNat {C : ℕ∞Sort u_1} (d : C ) (f : (a : ) → C a) (x : ) [x.AtLeastTwo] :
= f (OfNat.ofNat x)
@[simp]
theorem ENat.top_ne_coe (a : ) :
a
@[simp]
theorem ENat.top_ne_ofNat (a : ) [a.AtLeastTwo] :
@[simp]
@[simp]
@[simp]
theorem ENat.coe_ne_top (a : ) :
a
@[simp]
theorem ENat.ofNat_ne_top (a : ) [a.AtLeastTwo] :
@[simp]
@[simp]
@[simp]
theorem ENat.top_sub_coe (a : ) :
- a =
@[simp]
@[simp]
theorem ENat.top_sub_ofNat (a : ) [a.AtLeastTwo] :
@[simp]
theorem ENat.sub_top (a : ℕ∞) :
a - = 0
@[simp]
theorem ENat.coe_toNat_eq_self {n : ℕ∞} :
n.toNat = n n
theorem ENat.coe_toNat {n : ℕ∞} :
n n.toNat = n

Alias of the reverse direction of ENat.coe_toNat_eq_self.

theorem ENat.coe_toNat_le_self (n : ℕ∞) :
n.toNat n
theorem ENat.toNat_add {m : ℕ∞} {n : ℕ∞} (hm : m ) (hn : n ) :
(m + n).toNat = m.toNat + n.toNat
theorem ENat.toNat_sub {n : ℕ∞} (hn : n ) (m : ℕ∞) :
(m - n).toNat = m.toNat - n.toNat
theorem ENat.toNat_eq_iff {m : ℕ∞} {n : } (hn : n 0) :
m.toNat = n m = n
theorem ENat.toNat_le_of_le_coe {m : ℕ∞} {n : } (h : m n) :
m.toNat n
theorem ENat.toNat_le_toNat {m : ℕ∞} {n : ℕ∞} (h : m n) (hn : n ) :
m.toNat n.toNat
@[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
@[deprecated Order.one_le_iff_pos]
theorem ENat.one_le_iff_pos {n : ℕ∞} :
1 n 0 < n
theorem ENat.lt_one_iff_eq_zero {n : ℕ∞} :
n < 1 n = 0
theorem ENat.le_of_lt_add_one {m : ℕ∞} {n : ℕ∞} (h : m < n + 1) :
m n
theorem ENat.lt_add_one_iff {m : ℕ∞} {n : ℕ∞} (hm : n ) :
m < n + 1 m n
theorem ENat.le_coe_iff {n : ℕ∞} {k : } :
n k ∃ (n₀ : ), n = n₀ n₀ k
@[simp]
theorem ENat.not_lt_zero (n : ℕ∞) :
¬n < 0
@[simp]
theorem ENat.coe_lt_top (n : ) :
n <
theorem ENat.nat_induction {P : } (a : ℕ∞) (h0 : P 0) (hsuc : ∀ (n : ), P nP n.succ) (htop : (∀ (n : ), P n)P ) :
P a