# mathlibdocumentation

data.nat.part_enat

# Natural numbers with infinity #

The natural numbers and an extra top element ⊤. This implementation uses part ℕ as an implementation. Use ℕ∞ instead unless you care about computability.

## Main definitions #

The following instances are defined:

• ordered_add_comm_monoid part_enat
• canonically_ordered_add_monoid part_enat

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

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

• with_top_add_equiv : part_enat ≃+ ℕ∞

• with_top_order_iso : part_enat ≃o ℕ∞

## Implementation details #

part_enat is defined to be part ℕ.

+ and ≤ are defined on part_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 part_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 #

part_enat, ℕ∞

def part_enat  :
Type

Type of natural numbers with infinity (⊤)

Equations
Instances for part_enat
def part_enat.some  :

The computable embedding ℕ → part_enat.

This coincides with the coercion coe : ℕ → part_enat, see part_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]
Equations
@[simp]
theorem part_enat.dom_some (x : ) :
@[protected, instance]
Equations
@[protected, instance]
Equations
theorem part_enat.some_eq_coe (n : ) :
@[simp]
theorem part_enat.coe_inj {x y : } :
x = y x = y
@[simp]
theorem part_enat.dom_coe (x : ) :
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
theorem part_enat.le_def (x y : part_enat) :
x y ∃ (h : y.dom → x.dom), ∀ (hy : y.dom), x.get _ y.get hy
@[protected]
theorem part_enat.cases_on' {P : part_enat → Prop} (a : part_enat) :
P (∀ (n : ), P (part_enat.some n))P a
@[protected]
theorem part_enat.cases_on {P : part_enat → Prop} (a : part_enat) :
P (∀ (n : ), P n)P a
@[simp]
theorem part_enat.top_add (x : part_enat) :
@[simp]
theorem part_enat.add_top (x : part_enat) :
@[simp]
theorem part_enat.coe_get {x : part_enat} (h : x.dom) :
(x.get h) = x
@[simp, norm_cast]
theorem part_enat.get_coe' (x : ) (h : x.dom) :
x.get h = x
theorem part_enat.get_coe {x : } :
x.get _ = x
theorem part_enat.coe_add_get {x : } {y : part_enat} (h : (x + y).dom) :
(x + y).get h = x + y.get _
@[simp]
theorem part_enat.get_add {x y : part_enat} (h : (x + y).dom) :
(x + y).get h = x.get _ + y.get _
@[simp]
theorem part_enat.get_zero (h : 0.dom) :
0.get h = 0
@[simp]
theorem part_enat.get_one (h : 1.dom) :
1.get h = 1
theorem part_enat.get_eq_iff_eq_some {a : part_enat} {ha : a.dom} {b : } :
a.get ha = b
theorem part_enat.get_eq_iff_eq_coe {a : part_enat} {ha : a.dom} {b : } :
a.get ha = b a = b
theorem part_enat.dom_of_le_of_dom {x y : part_enat} :
x yy.dom → x.dom
theorem part_enat.dom_of_le_some {x : part_enat} {y : } (h : x ) :
x.dom
theorem part_enat.dom_of_le_coe {x : part_enat} {y : } (h : x y) :
x.dom
@[protected, instance]
Equations

The coercion ℕ → part_enat preserves 0 and addition.

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

Computably converts an part_enat to a ℕ∞.

Equations
@[simp]
@[simp]
theorem part_enat.to_with_top_coe' (n : ) {h : decidable n.dom} :
@[simp]
@[simp]
@[simp]
noncomputable def part_enat.with_top_equiv  :

equiv between part_enat and ℕ∞ (for the order isomorphism see with_top_order_iso).

Equations
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
noncomputable def part_enat.with_top_order_iso  :

to_with_top induces an order isomorphism between part_enat and ℕ∞.

Equations
@[simp]
@[simp]
@[simp]
@[simp]
theorem part_enat.with_top_equiv_symm_lt {x y : ℕ∞} :
x < y

to_with_top induces an additive monoid isomorphism between part_enat and ℕ∞.

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

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

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