mathlib documentation

data.nat.enat

Natural numbers with infinity

The natural numbers and an extra top element .

Main definitions

The following instances are defined:

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

Implementation details

enat is defined to be roption.

+ 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
@[instance]

Equations
@[instance]

Equations
@[instance]

Equations
@[instance]

Equations
@[instance]

Equations
@[simp]
theorem enat.coe_inj {x y : } :
x = y x = y

@[instance]

Equations
@[instance]

Equations
@[instance]

Equations
@[instance]

Equations
@[instance]

Equations
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_zero  :
0 = 0

@[simp]
theorem enat.coe_one  :
1 = 1

@[simp]
theorem enat.coe_add (x y : ) :
(x + y) = x + y

@[simp]
theorem enat.get_coe {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.coe_get {x : enat} (h : x.dom) :
(x.get h) = x

@[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.dom_of_le_some {x : enat} {y : } :
x y → x.dom

The coercion ℕ → enat preserves 0 and addition.

Equations
@[instance]

Equations
@[simp]
theorem enat.coe_le_coe {x y : } :
x y x y

@[simp]
theorem enat.coe_lt_coe {x y : } :
x < y x < y

theorem enat.get_le_get {x y : enat} {hx : x.dom} {hy : y.dom} :
x.get hx y.get hy x y

theorem enat.zero_lt_one  :
0 < 1

@[instance]

Equations
theorem enat.coe_lt_top (x : ) :

@[simp]
theorem enat.coe_ne_top (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} :
x < yx

theorem enat.pos_iff_one_le {x : enat} :
0 < x 1 x

theorem enat.sup_eq_max {a b : enat} :
a b = max a b

theorem enat.inf_eq_min {a b : enat} :
a b = min a b

theorem enat.add_lt_add_right {x y z : enat} :
x < yz x + z < y + z

theorem enat.add_lt_add_iff_right {x y z : enat} :
z (x + z < y + z x < y)

theorem enat.add_lt_add_iff_left {x y z : enat} :
z (z + x < z + y x < y)

theorem enat.lt_add_iff_pos_right {x y : enat} :
x (x < x + y 0 < y)

theorem enat.lt_add_one {x : enat} :
x x < x + 1

theorem enat.le_of_lt_add_one {x y : enat} :
x < y + 1x y

theorem enat.add_one_le_of_lt {x y : enat} :
x < yx + 1 y

theorem enat.add_one_le_iff_lt {x y : enat} :
x (x + 1 y x < y)

theorem enat.lt_add_one_iff_lt {x y : enat} :
x (x < y + 1 x y)

theorem enat.add_eq_top_iff {a b : enat} :
a + b = a = b =

theorem enat.add_right_cancel_iff {a b c : enat} :
c (a + c = b + c a = b)

theorem enat.add_left_cancel_iff {a b c : enat} :
a (a + b = a + c b = c)

Computably converts an enat to a with_top.

Equations
@[simp]

@[simp]

@[simp]

@[simp]

@[simp]

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

Equations

to_with_top induces an order isomorphism between enat and with_top.

Equations

to_with_top induces an additive monoid isomorphism between enat and with_top.

Equations