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

@[simp]
theorem enat.dom_coe (x : ) :

@[instance]

Equations
@[instance]

Equations
@[instance]

Equations
@[instance]

Equations
@[instance]

Equations
theorem enat.le_def (x y : enat) :
x y ∃ (h : y.dom → x.dom), ∀ (hy : y.dom), x.get _ y.get hy

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

theorem enat.get_coe {x : } :

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

theorem enat.dom_of_le_some {x : enat} {y : } (h : x y) :
x.dom

@[instance]
def enat.decidable_le (x y : enat) [decidable x.dom] [decidable y.dom] :

Equations

The coercion ℕ → enat preserves 0 and addition.

Equations
@[instance]

Equations
theorem enat.lt_def (x y : enat) :
x < y ∃ (hx : x.dom), ∀ (hy : y.dom), x.get hx < y.get hy

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

@[simp]
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

theorem enat.zero_lt_one  :
0 < 1

@[instance]

Equations
theorem enat.dom_of_lt {x y : enat} :
x < y → x.dom

@[simp]
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} (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

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} (h : x < y) (hz : z ) :
x + z < y + z

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

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

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 =

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

theorem enat.add_left_cancel_iff {a b c : enat} (ha : 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
def enat.find (P : → Prop) [decidable_pred P] :

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

Equations
@[simp]
theorem enat.find_get (P : → Prop) [decidable_pred P] (h : (enat.find P).dom) :

theorem enat.find_dom (P : → Prop) [decidable_pred P] (h : ∃ (n : ), P n) :

theorem enat.lt_find (P : → Prop) [decidable_pred P] (n : ) (h : ∀ (m : ), m n¬P m) :

theorem enat.lt_find_iff (P : → Prop) [decidable_pred P] (n : ) :
n < enat.find P ∀ (m : ), m n¬P m

theorem enat.find_le (P : → Prop) [decidable_pred P] (n : ) (h : P n) :

theorem enat.find_eq_top_iff (P : → Prop) [decidable_pred P] :
enat.find P = ∀ (n : ), ¬P n