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.

def ENat :

Extended natural numbers ℕ∞ = WithTop ℕ∞ = WithTop ℕ.

Equations

Extended natural numbers ℕ∞ = WithTop ℕ∞ = WithTop ℕ.

Equations
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
Equations

Conversion of ℕ∞∞ to sending ∞∞ to 0.

Equations
@[simp]
theorem ENat.toNat_coe (n : ) :
ENat.toNat n = n
@[simp]
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↑a.

Equations
@[simp]
theorem ENat.recTopCoe_top {C : ℕ∞Sort u_1} (d : C ) (f : (a : ) → C a) :
@[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 : ℕ∞} :
↑(ENat.toNat n) = n n
theorem ENat.coe_toNat {n : ℕ∞} :
n ↑(ENat.toNat n) = n

Alias of the reverse direction of ENat.coe_toNat_eq_self.

theorem ENat.toNat_add {m : ℕ∞} {n : ℕ∞} (hm : m ) (hn : n ) :
ENat.toNat (m + n) = ENat.toNat m + ENat.toNat n
theorem ENat.toNat_sub {n : ℕ∞} (hn : n ) (m : ℕ∞) :
ENat.toNat (m - n) = ENat.toNat m - ENat.toNat n
theorem ENat.toNat_eq_iff {m : ℕ∞} {n : } (hn : n 0) :
ENat.toNat m = n m = n
@[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.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 ↑(Nat.succ n)) (htop : ((n : ) → P n) → P ) :
P a