data.nat.enat

# Natural numbers with infinity #

The natural numbers and an extra top element ⊤.

## Main definitions #

The following instances are defined:

• ordered_add_comm_monoid enat
• canonically_ordered_add_monoid enat

There is no additive analogue of monoid_with_zero; if there were then enat could be an add_monoid_with_top.

• to_with_top : the map from enat to with_top ℕ, with theorems that it plays well with + and ≤.

• with_top_add_equiv : enat ≃+ with_top ℕ

• with_top_order_iso : enat ≃o with_top ℕ

## Implementation details #

enat is defined to be part ℕ.

+ and ≤ are defined on enat, but there is an issue with * because it's not clear what 0 * ⊤ should be. mul is hence left undefined. Similarly ⊤ - ⊤ is ambiguous so there is no - defined on enat.

Before the open_locale classical line, various proofs are made with decidability assumptions. This can cause issues -- see for example the non-simp lemma to_with_top_zero proved by rfl, followed by @[simp] lemma to_with_top_zero' whose proof uses convert.

## Tags #

enat, with_top ℕ

def enat  :
Type

Type of natural numbers with infinity (⊤)

Equations
Instances for enat
def enat.some  :

The computable embedding ℕ → enat.

This coincides with the coercion coe : ℕ → enat, see enat.some_eq_coe. However, coe is noncomputable so some is preferable when computability is a concern.

Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
def enat.dom.decidable (n : ) :
Equations
@[simp]
theorem enat.dom_some (x : ) :
@[protected, instance]
Equations
@[protected, instance]
Equations
theorem enat.some_eq_coe (n : ) :
= n
@[simp]
theorem enat.coe_inj {x y : } :
x = y x = y
@[simp]
theorem enat.dom_coe (x : ) :
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
theorem enat.le_def (x y : enat) :
x y ∃ (h : y.dom → x.dom), ∀ (hy : y.dom), x.get _ y.get hy
@[protected]
theorem enat.cases_on' {P : enat → Prop} (a : enat) :
P (∀ (n : ), P (enat.some n))P a
@[protected]
theorem enat.cases_on {P : enat → Prop} (a : enat) :
P (∀ (n : ), P n)P a
@[simp]
theorem enat.top_add (x : enat) :
@[simp]
theorem enat.add_top (x : enat) :
@[simp]
theorem enat.coe_get {x : enat} (h : x.dom) :
(x.get h) = x
@[simp, norm_cast]
theorem enat.get_coe' (x : ) (h : x.dom) :
x.get h = x
theorem enat.get_coe {x : } :
x.get _ = x
theorem enat.coe_add_get {x : } {y : enat} (h : (x + y).dom) :
(x + y).get h = x + y.get _
@[simp]
theorem enat.get_add {x y : enat} (h : (x + y).dom) :
(x + y).get h = x.get _ + y.get _
@[simp]
theorem enat.get_zero (h : 0.dom) :
0.get h = 0
@[simp]
theorem enat.get_one (h : 1.dom) :
1.get h = 1
theorem enat.get_eq_iff_eq_some {a : enat} {ha : a.dom} {b : } :
a.get ha = b a =
theorem enat.get_eq_iff_eq_coe {a : enat} {ha : a.dom} {b : } :
a.get ha = b a = b
theorem enat.dom_of_le_of_dom {x y : enat} :
x yy.dom → x.dom
theorem enat.dom_of_le_some {x : enat} {y : } (h : x ) :
x.dom
theorem enat.dom_of_le_coe {x : enat} {y : } (h : x y) :
x.dom
@[protected, instance]
def enat.decidable_le (x y : enat) [decidable x.dom] [decidable y.dom] :
Equations
def enat.coe_hom  :

The coercion ℕ → enat preserves 0 and addition.

Equations
@[simp]
theorem enat.coe_coe_hom  :
@[protected, instance]
Equations
theorem enat.lt_def (x y : enat) :
x < y ∃ (hx : x.dom), ∀ (hy : y.dom), x.get hx < y.get hy
@[simp, norm_cast]
theorem enat.coe_le_coe {x y : } :
x y x y
@[simp, norm_cast]
theorem enat.coe_lt_coe {x y : } :
x < y x < y
@[simp]
theorem enat.get_le_get {x y : enat} {hx : x.dom} {hy : y.dom} :
x.get hx y.get hy x y
theorem enat.le_coe_iff (x : enat) (n : ) :
x n ∃ (h : x.dom), x.get h n
theorem enat.lt_coe_iff (x : enat) (n : ) :
x < n ∃ (h : x.dom), x.get h < n
theorem enat.coe_le_iff (n : ) (x : enat) :
n x ∀ (h : x.dom), n x.get h
theorem enat.coe_lt_iff (n : ) (x : enat) :
n < x ∀ (h : x.dom), n < x.get h
@[protected]
theorem enat.zero_lt_one  :
0 < 1
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
theorem enat.eq_zero_iff {x : enat} :
x = 0 x 0
theorem enat.ne_zero_iff {x : enat} :
x 0 < x
theorem enat.dom_of_lt {x y : enat} :
x < y → x.dom
theorem enat.top_eq_none  :
@[simp]
theorem enat.coe_lt_top (x : ) :
@[simp]
theorem enat.coe_ne_top (x : ) :
theorem enat.not_is_max_coe (x : ) :
theorem enat.ne_top_iff {x : enat} :
x ∃ (n : ), x = n
theorem enat.ne_top_iff_dom {x : enat} :
theorem enat.ne_top_of_lt {x y : enat} (h : x < y) :
theorem enat.eq_top_iff_forall_lt (x : enat) :
x = ∀ (n : ), n < x
theorem enat.eq_top_iff_forall_le (x : enat) :
x = ∀ (n : ), n x
theorem enat.pos_iff_one_le {x : enat} :
0 < x 1 x
@[protected, instance]
@[protected, instance]
noncomputable def enat.linear_order  :
Equations
@[protected, instance]
Equations
@[protected, instance]
noncomputable def enat.lattice  :
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected]
theorem enat.add_lt_add_right {x y z : enat} (h : x < y) (hz : z ) :
x + z < y + z
@[protected]
theorem enat.add_lt_add_iff_right {x y z : enat} (hz : z ) :
x + z < y + z x < y
@[protected]
theorem enat.add_lt_add_iff_left {x y z : enat} (hz : z ) :
z + x < z + y x < y
@[protected]
theorem enat.lt_add_iff_pos_right {x y : enat} (hx : x ) :
x < x + y 0 < y
theorem enat.lt_add_one {x : enat} (hx : x ) :
x < x + 1
theorem enat.le_of_lt_add_one {x y : enat} (h : x < y + 1) :
x y
theorem enat.add_one_le_of_lt {x y : enat} (h : x < y) :
x + 1 y
theorem enat.add_one_le_iff_lt {x y : enat} (hx : x ) :
x + 1 y x < y
theorem enat.lt_add_one_iff_lt {x y : enat} (hx : x ) :
x < y + 1 x y
theorem enat.add_eq_top_iff {a b : enat} :
a + b = a = b =
@[protected]
theorem enat.add_right_cancel_iff {a b c : enat} (hc : c ) :
a + c = b + c a = b
@[protected]
theorem enat.add_left_cancel_iff {a b c : enat} (ha : a ) :
a + b = a + c b = c
def enat.to_with_top (x : enat) [decidable x.dom] :

Computably converts an enat to a with_top ℕ.

Equations
@[simp]
@[simp]
theorem enat.to_with_top_coe (n : ) {_x : decidable n.dom} :
@[simp]
theorem enat.to_with_top_coe' (n : ) {h : decidable n.dom} :
@[simp]
theorem enat.to_with_top_le {x y : enat} [decidable x.dom] [decidable y.dom] :
x y
@[simp]
theorem enat.to_with_top_lt {x y : enat} [decidable x.dom] [decidable y.dom] :
x < y
@[simp]
theorem enat.to_with_top_add {x y : enat} :
(x + y).to_with_top =
noncomputable def enat.with_top_equiv  :

equiv between enat and with_top ℕ (for the order isomorphism see with_top_order_iso).

Equations
@[simp]
@[simp]
theorem enat.with_top_equiv_coe (n : ) :
@[simp]
@[simp]
theorem enat.with_top_equiv_le {x y : enat} :
@[simp]
theorem enat.with_top_equiv_lt {x y : enat} :
noncomputable def enat.with_top_order_iso  :

to_with_top induces an order isomorphism between enat and with_top ℕ.

Equations
@[simp]
@[simp]
@[simp]
@[simp]
theorem enat.with_top_equiv_symm_lt {x y : with_top } :
x < y
noncomputable def enat.with_top_add_equiv  :

to_with_top induces an additive monoid isomorphism between enat and with_top ℕ.

Equations
theorem enat.lt_wf  :
@[protected, instance]
@[protected, instance]
Equations
def enat.find (P : → Prop)  :

The smallest enat satisfying a (decidable) predicate P : ℕ → Prop

Equations
@[simp]
theorem enat.find_get (P : → Prop) (h : (enat.find P).dom) :
(enat.find P).get h =
theorem enat.find_dom (P : → Prop) (h : ∃ (n : ), P n) :
theorem enat.lt_find (P : → Prop) (n : ) (h : ∀ (m : ), m n¬P m) :
n <
theorem enat.lt_find_iff (P : → Prop) (n : ) :
n < ∀ (m : ), m n¬P m
theorem enat.find_le (P : → Prop) (n : ) (h : P n) :
theorem enat.find_eq_top_iff (P : → Prop)  :
∀ (n : ), ¬P n
@[protected, instance]
Equations