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

source
def enat  :
Type

Extended natural numbers ℕ∞ = with_top ℕ.

Equations
Instances for enat
source
@[protected, instance]
def enat.has_zero  :
has_zero ℕ∞
source
@[protected, instance]
def enat.has_well_founded  :
has_well_founded ℕ∞
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.well_founded_lt  :
well_founded_lt ℕ∞
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.char_zero  :
char_zero ℕ∞
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]
def enat.has_coe_t  :
has_coe_t ℕ ℕ∞
source
@[protected, instance]
def enat.has_bot  :
has_bot ℕ∞
source
@[protected, instance]
def enat.inhabited  :
inhabited ℕ∞
Equations
source
@[protected, instance]
def enat.has_lt.lt.is_well_order  :
is_well_order ℕ∞ has_lt.lt
source
@[simp, norm_cast, nolint]
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.can_lift  :
can_lift ℕ∞ ℕ coe (λ (n : ℕ∞), n ≠ ⊤)
Equations
source
def enat.to_nat  :
ℕ∞ →*₀ ℕ

Conversion of ℕ∞ to ℕ sending ∞ to 0.

Equations
source
@[simp]
theorem enat.to_nat_coe (n : ℕ) :
⇑enat.to_nat ↑n = n
source
@[simp]
theorem enat.to_nat_top  :
⇑enat.to_nat ⊤ = 0
source
@[simp]
theorem enat.coe_to_nat_eq_self {n : ℕ∞} :
↑(⇑enat.to_nat n) = n ↔ n ≠ ⊤
source
theorem enat.coe_to_nat {n : ℕ∞} :
n ≠ ⊤ → ↑(⇑enat.to_nat n) = n

Alias of the reverse direction of enat.coe_to_nat_eq_self.

source
theorem enat.coe_to_nat_le_self (n : ℕ∞) :
↑(⇑enat.to_nat n) ≤ n
source
theorem enat.to_nat_add {m n : ℕ∞} (hm : m ≠ ⊤) (hn : n ≠ ⊤) :
⇑enat.to_nat (m + n) = ⇑enat.to_nat m + ⇑enat.to_nat n
source
theorem enat.to_nat_sub {n : ℕ∞} (hn : n ≠ ⊤) (m : ℕ∞) :
⇑enat.to_nat (m - n) = ⇑enat.to_nat m - ⇑enat.to_nat n
source
theorem enat.to_nat_eq_iff {m : ℕ∞} {n : ℕ} (hn : n ≠ 0) :
⇑enat.to_nat m = n ↔ m = ↑n
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