# Documentation

Mathlib.Data.Nat.PartENat

# 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
• CanonicallyOrderedAddMonoid 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 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 (⊤)

Instances For

The computable embedding ℕ → PartENat.

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

Instances For
@[simp]
theorem PartENat.dom_some (x : ) :
(x).Dom
theorem PartENat.some_eq_natCast (n : ) :
n = n
@[simp]
theorem PartENat.natCast_inj {x : } {y : } :
x = y x = y
@[simp]
theorem PartENat.dom_natCast (x : ) :
(x).Dom
theorem PartENat.le_def (x : PartENat) (y : PartENat) :
x y h, ∀ (hy : y.Dom), Part.get x (_ : x.Dom) Part.get y 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) :
↑(Part.get x h) = x
@[simp]
theorem PartENat.get_natCast' (x : ) (h : (x).Dom) :
Part.get (x) h = x
theorem PartENat.get_natCast {x : } :
Part.get x (_ : (x).Dom) = x
theorem PartENat.coe_add_get {x : } {y : PartENat} (h : (x + y).Dom) :
Part.get (x + y) h = x + Part.get y (_ : y.Dom)
@[simp]
theorem PartENat.get_add {x : PartENat} {y : PartENat} (h : (x + y).Dom) :
Part.get (x + y) h = Part.get x (_ : x.Dom) + Part.get y (_ : y.Dom)
@[simp]
theorem PartENat.get_zero (h : 0.Dom) :
Part.get 0 h = 0
@[simp]
theorem PartENat.get_one (h : 1.Dom) :
Part.get 1 h = 1
theorem PartENat.get_eq_iff_eq_some {a : PartENat} {ha : a.Dom} {b : } :
Part.get a ha = b a = b
theorem PartENat.get_eq_iff_eq_coe {a : PartENat} {ha : a.Dom} {b : } :
Part.get a 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] :

The coercion ℕ → PartENat preserves 0 and addition.

Instances For
@[simp]
theorem PartENat.lt_def (x : PartENat) (y : PartENat) :
x < y hx, ∀ (hy : y.Dom), Part.get x hx < Part.get y hy
@[simp]
theorem PartENat.coe_le_coe {x : } {y : } :
x y x y
@[simp]
theorem PartENat.coe_lt_coe {x : } {y : } :
x < y x < y
@[simp]
theorem PartENat.get_le_get {x : PartENat} {y : PartENat} {hx : x.Dom} {hy : y.Dom} :
Part.get x hx Part.get y hy x y
theorem PartENat.le_coe_iff (x : PartENat) (n : ) :
x n h, Part.get x h n
theorem PartENat.lt_coe_iff (x : PartENat) (n : ) :
x < n h, Part.get x h < n
theorem PartENat.coe_le_iff (n : ) (x : PartENat) :
n x ∀ (h : x.Dom), n Part.get x h
theorem PartENat.coe_lt_iff (n : ) (x : PartENat) :
n < x ∀ (h : x.Dom), n < Part.get x 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]
theorem PartENat.natCast_ne_top (x : ) :
x
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 => x x_1
noncomputable instance PartENat.linearOrder :
noncomputable instance PartENat.lattice :
theorem PartENat.eq_natCast_sub_of_add_eq_natCast {x : PartENat} {y : PartENat} {n : } (h : x + y = n) :
x = ↑(n - Part.get y (_ : y.Dom))
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} :
↑() 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 < ↑() 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 ℕ∞.

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

Coercion from ℕ∞ to PartENat.

Instances For
@[simp]
theorem PartENat.ofENat_none :
none =
@[simp]
theorem PartENat.ofENat_some (n : ) :
↑(some n) = n
@[simp]
theorem PartENat.toWithTop_ofENat (n : ℕ∞) :
∀ {x : Decidable (n).Dom},
@[simp]
noncomputable def PartENat.withTopEquiv :

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

Instances For
@[simp]
@[simp]
theorem PartENat.withTopEquiv_natCast (n : ) :
= n
@[simp]
@[simp]
theorem PartENat.withTopEquiv_lt {x : PartENat} {y : PartENat} :
x < y
noncomputable def PartENat.withTopOrderIso :

to_WithTop induces an order isomorphism between PartENat and ℕ∞.

Instances For
@[simp]
theorem PartENat.withTopEquiv_symm_coe (n : ) :
n = n
@[simp]
@[simp]
theorem PartENat.withTopEquiv_symm_le {x : ℕ∞} {y : ℕ∞} :
x y x y
@[simp]
theorem PartENat.withTopEquiv_symm_lt {x : ℕ∞} {y : ℕ∞} :
x < y x < y

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

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

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

Instances For
@[simp]
theorem PartENat.find_get (P : ) [] (h : ().Dom) :
=
theorem PartENat.find_dom (P : ) [] (h : n, P n) :
().Dom
theorem PartENat.lt_find (P : ) [] (n : ) (h : ∀ (m : ), m n¬P m) :
n <
theorem PartENat.lt_find_iff (P : ) [] (n : ) :
n < ∀ (m : ), m n¬P m
theorem PartENat.find_le (P : ) [] (n : ) (h : P n) :
n
theorem PartENat.find_eq_top_iff (P : ) [] :
∀ (n : ), ¬P n