# Documentation

Mathlib.Data.ENat.Basic

# 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.

def ENat :

Extended natural numbers ℕ∞ = WithTop ℕ.

Instances For

Extended natural numbers ℕ∞ = WithTop ℕ.

Instances For
@[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
theorem ENat.coe_mul (m : ) (n : ) :
↑(m * n) = m * n
instance ENat.canLift :
CanLift ℕ∞ Nat.cast fun n => n

Conversion of ℕ∞ to ℕ sending ∞ to 0.

Instances For
@[simp]
theorem ENat.toNat_coe (n : ) :
ENat.toNat n = n
@[simp]
theorem ENat.toNat_top :
= 0
def ENat.recTopCoe {C : ℕ∞Sort u_1} (h₁ : C ) (h₂ : (a : ) → C a) (n : ℕ∞) :
C n

Recursor for ENat using the preferred forms ⊤ and ↑a.

Instances For
@[simp]
theorem ENat.recTopCoe_top {C : ℕ∞Sort u_1} (d : C ) (f : (a : ) → C a) :
= d
@[simp]
theorem ENat.recTopCoe_coe {C : ℕ∞Sort u_1} (d : C ) (f : (a : ) → C a) (x : ) :
ENat.recTopCoe d f x = f x
@[simp]
theorem ENat.top_ne_coe (a : ) :
a
@[simp]
theorem ENat.coe_ne_top (a : ) :
a
@[simp]
theorem ENat.top_sub_coe (a : ) :
- a =
theorem ENat.sub_top (a : ℕ∞) :
a - = 0
@[simp]
theorem ENat.coe_toNat_eq_self {n : ℕ∞} :
↑() = n n
theorem ENat.coe_toNat {n : ℕ∞} :
n ↑() = n

Alias of the reverse direction of ENat.coe_toNat_eq_self.

theorem ENat.coe_toNat_le_self (n : ℕ∞) :
↑() n
theorem ENat.toNat_add {m : ℕ∞} {n : ℕ∞} (hm : m ) (hn : n ) :
ENat.toNat (m + n) = +
theorem ENat.toNat_sub {n : ℕ∞} (hn : n ) (m : ℕ∞) :
ENat.toNat (m - n) = -
theorem ENat.toNat_eq_iff {m : ℕ∞} {n : } (hn : n 0) :
= n 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.le_of_lt_add_one {m : ℕ∞} {n : ℕ∞} (h : m < n + 1) :
m n
theorem ENat.le_coe_iff {n : ℕ∞} {k : } :
n k n₀, n = n₀ n₀ k
theorem ENat.nat_induction {P : } (a : ℕ∞) (h0 : P 0) (hsuc : (n : ) → P nP ↑()) (htop : ((n : ) → P n) → P ) :
P a