# 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:

• OrderedAddCommMonoid PartENat
• CanonicallyOrderedAddCommMonoid PartENat
• CompleteLinearOrder PartENat

There is no additive analogue of MonoidWithZero; if there were then PartENat could be an AddMonoidWithTop.

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

• withTopAddEquiv : PartENat ≃+ ℕ∞

• withTopOrderIso : PartENat ≃o ℕ∞

## Implementation details #

PartENat is defined to be Part ℕ.

+ and ≤ are defined on PartENat, 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 PartENat.

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

## Tags #

PartENat, ℕ∞

Type of natural numbers with infinity (⊤)

Equations
Instances For

The computable embedding ℕ → PartENat.

This coincides with the coercion coe : ℕ → PartENat, see PartENat.some_eq_natCast.

Equations
Instances For
Equations
Equations
instance PartENat.instOne :
Equations
Equations
Equations
@[simp]
theorem PartENat.dom_some (x : ) :
(x).Dom
Equations
theorem PartENat.some_eq_natCast (n : ) :
n = n
Equations
theorem PartENat.natCast_inj {x : } {y : } :
x = y x = y

Alias of Nat.cast_inj specialized to PartENat -

@[simp]
theorem PartENat.dom_natCast (x : ) :
(x).Dom
@[simp]
theorem PartENat.dom_ofNat (x : ) [x.AtLeastTwo] :
().Dom
@[simp]
@[simp]
Equations
instance PartENat.instLE :
Equations
instance PartENat.instTop :
Equations
instance PartENat.instBot :
Equations
instance PartENat.instSup :
Equations
theorem PartENat.le_def (x : PartENat) (y : PartENat) :
x y ∃ (h : y.Domx.Dom), ∀ (hy : y.Dom), x.get y.get hy
theorem PartENat.casesOn' {P : } (a : PartENat) :
P (∀ (n : ), P n)P a
theorem PartENat.casesOn {P : } (a : PartENat) :
P (∀ (n : ), P n)P a
@[simp]
theorem PartENat.natCast_get {x : PartENat} (h : x.Dom) :
(x.get h) = x
@[simp]
theorem PartENat.get_natCast' (x : ) (h : (x).Dom) :
(x).get h = x
theorem PartENat.get_natCast {x : } :
(x).get = x
theorem PartENat.coe_add_get {x : } {y : PartENat} (h : (x + y).Dom) :
(x + y).get h = x + y.get
@[simp]
theorem PartENat.get_add {x : PartENat} {y : PartENat} (h : (x + y).Dom) :
(x + y).get h = x.get + y.get
@[simp]
theorem PartENat.get_zero (h : ) :
Part.get 0 h = 0
@[simp]
theorem PartENat.get_one (h : ) :
Part.get 1 h = 1
@[simp]
theorem PartENat.get_ofNat' (x : ) [x.AtLeastTwo] (h : ().Dom) :
().get h =
theorem PartENat.get_eq_iff_eq_some {a : PartENat} {ha : a.Dom} {b : } :
a.get ha = b a = b
theorem PartENat.get_eq_iff_eq_coe {a : PartENat} {ha : a.Dom} {b : } :
a.get ha = b a = b
theorem PartENat.dom_of_le_of_dom {x : PartENat} {y : PartENat} :
x yy.Domx.Dom
theorem PartENat.dom_of_le_some {x : PartENat} {y : } (h : x y) :
x.Dom
theorem PartENat.dom_of_le_natCast {x : PartENat} {y : } (h : x y) :
x.Dom
instance PartENat.decidableLe (x : PartENat) (y : PartENat) [Decidable x.Dom] [Decidable y.Dom] :
Equations
• x.decidableLe y = if hx : x.Dom then else if hy : y.Dom then else
theorem PartENat.lt_def (x : PartENat) (y : PartENat) :
x < y ∃ (hx : x.Dom), ∀ (hy : y.Dom), x.get hx < y.get hy
Equations
Equations
Equations
theorem PartENat.coe_le_coe {x : } {y : } :
x y x y

Alias of Nat.cast_le specialized to PartENat -

theorem PartENat.coe_lt_coe {x : } {y : } :
x < y x < y

Alias of Nat.cast_lt specialized to PartENat -

@[simp]
theorem PartENat.get_le_get {x : PartENat} {y : PartENat} {hx : x.Dom} {hy : y.Dom} :
x.get hx y.get hy x y
theorem PartENat.le_coe_iff (x : PartENat) (n : ) :
x n ∃ (h : x.Dom), x.get h n
theorem PartENat.lt_coe_iff (x : PartENat) (n : ) :
x < n ∃ (h : x.Dom), x.get h < n
theorem PartENat.coe_le_iff (n : ) (x : PartENat) :
n x ∀ (h : x.Dom), n x.get h
theorem PartENat.coe_lt_iff (n : ) (x : PartENat) :
n < x ∀ (h : x.Dom), n < x.get h
theorem PartENat.dom_of_lt {x : PartENat} {y : PartENat} :
x < yx.Dom
theorem PartENat.top_eq_none :
= Part.none
@[simp]
theorem PartENat.natCast_lt_top (x : ) :
x <
@[simp]
@[simp]
@[simp]
theorem PartENat.ofNat_lt_top (x : ) [x.AtLeastTwo] :
@[simp]
theorem PartENat.natCast_ne_top (x : ) :
x
@[simp]
@[simp]
theorem PartENat.ofNat_ne_top (x : ) [x.AtLeastTwo] :
theorem PartENat.ne_top_iff {x : PartENat} :
x ∃ (n : ), x = n
theorem PartENat.ne_top_of_lt {x : PartENat} {y : PartENat} (h : x < y) :
theorem PartENat.eq_top_iff_forall_lt (x : PartENat) :
x = ∀ (n : ), n < x
theorem PartENat.eq_top_iff_forall_le (x : PartENat) :
x = ∀ (n : ), n x
instance PartENat.isTotal :
IsTotal PartENat fun (x x_1 : PartENat) => x x_1
Equations
noncomputable instance PartENat.linearOrder :
Equations
• One or more equations did not get rendered due to their size.
Equations
noncomputable instance PartENat.lattice :
Equations
Equations
• One or more equations did not get rendered due to their size.
theorem PartENat.eq_natCast_sub_of_add_eq_natCast {x : PartENat} {y : PartENat} {n : } (h : x + y = n) :
x = (n - y.get )
theorem PartENat.add_lt_add_right {x : PartENat} {y : PartENat} {z : PartENat} (h : x < y) (hz : z ) :
x + z < y + z
theorem PartENat.add_lt_add_iff_right {x : PartENat} {y : PartENat} {z : PartENat} (hz : z ) :
x + z < y + z x < y
theorem PartENat.add_lt_add_iff_left {x : PartENat} {y : PartENat} {z : PartENat} (hz : z ) :
z + x < z + y x < y
theorem PartENat.lt_add_iff_pos_right {x : PartENat} {y : PartENat} (hx : x ) :
x < x + y 0 < y
theorem PartENat.lt_add_one {x : PartENat} (hx : x ) :
x < x + 1
theorem PartENat.le_of_lt_add_one {x : PartENat} {y : PartENat} (h : x < y + 1) :
x y
theorem PartENat.add_one_le_of_lt {x : PartENat} {y : PartENat} (h : x < y) :
x + 1 y
theorem PartENat.add_one_le_iff_lt {x : PartENat} {y : PartENat} (hx : x ) :
x + 1 y x < y
theorem PartENat.coe_succ_le_iff {n : } {e : PartENat} :
n.succ e n < e
theorem PartENat.lt_add_one_iff_lt {x : PartENat} {y : PartENat} (hx : x ) :
x < y + 1 x y
theorem PartENat.lt_coe_succ_iff_le {x : PartENat} {n : } (hx : x ) :
x < n.succ x n
theorem PartENat.add_right_cancel_iff {a : PartENat} {b : PartENat} {c : PartENat} (hc : c ) :
a + c = b + c a = b
theorem PartENat.add_left_cancel_iff {a : PartENat} {b : PartENat} {c : PartENat} (ha : a ) :
a + b = a + c b = c

Computably converts a PartENat to a ℕ∞.

Equations
• x.toWithTop =
Instances For
theorem PartENat.toWithTop_top :
let_fun this := Part.noneDecidable; .toWithTop =
@[simp]
theorem PartENat.toWithTop_top' {h : Decidable .Dom} :
.toWithTop =
theorem PartENat.toWithTop_zero :
let_fun this := ;
@[simp]
theorem PartENat.toWithTop_zero' {h : } :
theorem PartENat.toWithTop_one :
let_fun this := ;
@[simp]
theorem PartENat.toWithTop_one' {h : } :
theorem PartENat.toWithTop_some (n : ) :
(n).toWithTop = n
theorem PartENat.toWithTop_natCast (n : ) :
∀ {x : Decidable (n).Dom}, (n).toWithTop = n
@[simp]
theorem PartENat.toWithTop_natCast' (n : ) :
∀ {x : Decidable (n).Dom}, (n).toWithTop = n
@[simp]
theorem PartENat.toWithTop_ofNat (n : ) [n.AtLeastTwo] :
∀ {x : Decidable ()}, ().toWithTop =
@[simp]
theorem PartENat.toWithTop_le {x : PartENat} {y : PartENat} [hx : Decidable x.Dom] [hy : Decidable y.Dom] :
x.toWithTop y.toWithTop x y
@[simp]
theorem PartENat.toWithTop_lt {x : PartENat} {y : PartENat} [Decidable x.Dom] [Decidable y.Dom] :
x.toWithTop < y.toWithTop x < y

Coercion from ℕ∞ to PartENat.

Equations
• x = match x with | none => Part.none | some n => n
Instances For
@[simp]
@[simp]
theorem PartENat.ofENat_coe (n : ) :
n = n
@[simp]
theorem PartENat.ofENat_zero :
0 = 0
@[simp]
theorem PartENat.ofENat_one :
1 = 1
@[simp]
theorem PartENat.ofENat_ofNat (n : ) [n.AtLeastTwo] :
() =
@[simp]
theorem PartENat.toWithTop_ofENat (n : ℕ∞) :
∀ {x : Decidable (n).Dom}, (n).toWithTop = n
@[simp]
theorem PartENat.ofENat_toWithTop (x : PartENat) :
∀ {x_1 : Decidable x.Dom}, x.toWithTop = x
@[simp]
theorem PartENat.ofENat_le {x : ℕ∞} {y : ℕ∞} :
x y x y
@[simp]
theorem PartENat.ofENat_lt {x : ℕ∞} {y : ℕ∞} :
x < y x < y
@[simp]
theorem PartENat.toWithTop_add {x : PartENat} {y : PartENat} :
(x + y).toWithTop = x.toWithTop + y.toWithTop
@[simp]
theorem PartENat.withTopEquiv_apply (x : PartENat) :
PartENat.withTopEquiv x = x.toWithTop
@[simp]
noncomputable def PartENat.withTopEquiv :

Equiv between PartENat and ℕ∞ (for the order isomorphism see withTopOrderIso).

Equations
Instances For
theorem PartENat.withTopEquiv_top :
PartENat.withTopEquiv =
theorem PartENat.withTopEquiv_natCast (n : ) :
PartENat.withTopEquiv n = n
theorem PartENat.withTopEquiv_zero :
PartENat.withTopEquiv 0 = 0
theorem PartENat.withTopEquiv_one :
PartENat.withTopEquiv 1 = 1
theorem PartENat.withTopEquiv_ofNat (n : ) [n.AtLeastTwo] :
PartENat.withTopEquiv () =
theorem PartENat.withTopEquiv_le {x : PartENat} {y : PartENat} :
PartENat.withTopEquiv x PartENat.withTopEquiv y x y
theorem PartENat.withTopEquiv_lt {x : PartENat} {y : PartENat} :
PartENat.withTopEquiv x < PartENat.withTopEquiv y x < y
theorem PartENat.withTopEquiv_symm_coe (n : ) :
n = n
theorem PartENat.withTopEquiv_symm_ofNat (n : ) [n.AtLeastTwo] :
() =
theorem PartENat.withTopEquiv_symm_lt {x : ℕ∞} {y : ℕ∞} :
x < y x < y
noncomputable def PartENat.withTopOrderIso :

toWithTop induces an order isomorphism between PartENat and ℕ∞.

Equations
Instances For

toWithTop induces an additive monoid isomorphism between PartENat and ℕ∞.

Equations
Instances For
theorem PartENat.lt_wf :
WellFounded fun (x x_1 : PartENat) => x < x_1
Equations
instance PartENat.isWellOrder :
IsWellOrder PartENat fun (x x_1 : PartENat) => x < x_1
Equations
Equations
def PartENat.find (P : ) [] :

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

Equations
• = { Dom := ∃ (n : ), P n, get := Nat.find }
Instances For
@[simp]
theorem PartENat.find_get (P : ) [] (h : ().Dom) :
().get h =
theorem PartENat.find_dom (P : ) [] (h : ∃ (n : ), P n) :
().Dom
theorem PartENat.lt_find (P : ) [] (n : ) (h : mn, ¬P m) :
n <
theorem PartENat.lt_find_iff (P : ) [] (n : ) :
n < mn, ¬P m
theorem PartENat.find_le (P : ) [] (n : ) (h : P n) :
n
theorem PartENat.find_eq_top_iff (P : ) [] :
∀ (n : ), ¬P n
Equations
• One or more equations did not get rendered due to their size.
noncomputable instance PartENat.instCompleteLinearOrder :
Equations
• One or more equations did not get rendered due to their size.