mathlib documentation

data.nat.enat

Definition and basic properties of extended natural numbers #

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

source
def enat  :
Type

Extended natural numbers ℕ∞ = with_top ℕ.

Equations
Instances for enat
source
@[protected, instance]
noncomputable def enat.complete_linear_order  :
complete_linear_order ℕ∞
source
@[protected, instance]
def enat.has_zero  :
has_zero ℕ∞
source
@[protected, instance]
def enat.order_bot  :
order_bot ℕ∞
source
@[protected, instance]
def enat.has_top  :
has_top ℕ∞
source
@[protected, instance]
def enat.has_sub  :
has_sub ℕ∞
source
@[protected, instance]
def enat.order_top  :
order_top ℕ∞
source
@[protected, instance]
def enat.nontrivial  :
nontrivial ℕ∞
source
@[protected, instance]
def enat.canonically_linear_ordered_add_monoid  :
canonically_linear_ordered_add_monoid ℕ∞
source
@[protected, instance]
def enat.add_comm_monoid_with_one  :
add_comm_monoid_with_one ℕ∞
source
@[protected, instance]
def enat.linear_ordered_add_comm_monoid_with_top  :
linear_ordered_add_comm_monoid_with_top ℕ∞
source
@[protected, instance]
def enat.canonically_ordered_comm_semiring  :
canonically_ordered_comm_semiring ℕ∞
source
@[protected, instance]
def enat.has_ordered_sub  :
has_ordered_sub ℕ∞
source
@[protected, instance]
def enat.succ_order  :
succ_order ℕ∞
source
@[protected, instance]
def enat.linear_order  :
linear_order ℕ∞
source
@[protected, instance]
noncomputable def enat.has_bot  :
has_bot ℕ∞
source
@[protected, instance]
def enat.inhabited  :
inhabited ℕ∞
Equations
source
@[simp, norm_cast]
theorem enat.coe_zero  :
↑0 = 0
source
@[simp, norm_cast]
theorem enat.coe_one  :
↑1 = 1
source
@[simp, norm_cast]
theorem enat.coe_add (m n : ℕ) :
↑(m + n) = ↑m + ↑n
source
@[simp, norm_cast]
theorem enat.coe_sub (m n : ℕ) :
↑(m - n) = ↑m - ↑n
source
@[simp, norm_cast]
theorem enat.coe_mul (m n : ℕ) :
↑(m * n) = ↑m * ↑n
source
@[protected, instance]
def enat.nat.can_lift  :
can_lift ℕ∞ ℕ
Equations
source
def enat.to_nat  :
ℕ∞ →*₀ ℕ

Conversion of ℕ∞ to ℕ sending ∞ to 0.

Equations
source
@[simp]
theorem enat.succ_def (m : ℕ∞) :
order.succ m = m + 1
source
theorem enat.add_one_le_of_lt {m n : ℕ∞} (h : m < n) :
m + 1 ≤ n
source
theorem enat.add_one_le_iff {m n : ℕ∞} (hm : m ≠ ⊤) :
m + 1 ≤ n ↔ m < n
source
theorem enat.one_le_iff_pos {n : ℕ∞} :
1 ≤ n ↔ 0 < n
source
theorem enat.one_le_iff_ne_zero {n : ℕ∞} :
1 ≤ n ↔ n ≠ 0
source
theorem enat.le_of_lt_add_one {m n : ℕ∞} (h : m < n + 1) :
m ≤ n
source
theorem enat.nat_induction {P : ℕ∞ → Prop} (a : ℕ∞) (h0 : P 0) (hsuc : ∀ (n : ℕ), P ↑n → P ↑(n.succ)) (htop : (∀ (n : ℕ), P ↑n) → P ⊤) :
P a