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 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
def enat.some  :
enat

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
@[instance]
Equations
@[instance]
Equations
@[instance]
Equations
@[instance]
Equations
theorem enat.some_eq_coe (n : ) :
@[simp]
theorem enat.coe_inj {x y : } :
x = y x = y
@[simp]
theorem enat.dom_some (x : ) :
@[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 (enat.some n))P a
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]
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 = enat.some b
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 enat.some y) :
x.dom
theorem enat.dom_of_le_coe {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