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
• CanonicallyOrderedAdd 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.

Deprecation

As it appears this has been unused since 2018, we are now deprecating it. If ENat does not serve your purposes, please raise this on the community Zulip.

Tags

PartENat, ℕ∞

@[deprecated ENat (since := "2025-09-01")]

def PartENat : Type

Type of natural numbers with infinity (⊤)

Equations

• PartENat = Part ℕ

def PartENat.some : ℕ → PartENat

The computable embedding ℕ → PartENat.

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

Equations

• PartENat.some = Part.some

instance PartENat.instZero : Zero PartENat

Equations

• PartENat.instZero = { zero := ↑0 }

instance PartENat.instInhabited : Inhabited PartENat

Equations

• PartENat.instInhabited = { default := 0 }

instance PartENat.instOne : One PartENat

Equations

• PartENat.instOne = { one := ↑1 }

instance PartENat.instAdd : Add PartENat

Equations

• PartENat.instAdd = { add := fun (x y : PartENat) => { Dom := x.Dom ∧ y.Dom, get := fun (h : x.Dom ∧ y.Dom) => x.get ⋯ + y.get ⋯ } }

instance PartENat.instDecidableDomNatSome (n : ℕ) : Decidable (↑n).Dom

Equations

• PartENat.instDecidableDomNatSome n = isTrue trivial

@[simp]

theorem PartENat.dom_some (x : ℕ) : (↑x).Dom

instance PartENat.addCommMonoid : AddCommMonoid PartENat

Equations

• One or more equations did not get rendered due to their size.

instance PartENat.instAddCommMonoidWithOne : AddCommMonoidWithOne PartENat

Equations

• One or more equations did not get rendered due to their size.

theorem PartENat.some_eq_natCast (n : ℕ) : ↑n = ↑n

instance PartENat.instCharZero : CharZero PartENat

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] : (OfNat.ofNat x).Dom

@[simp]

theorem PartENat.dom_zero : Part.Dom 0

@[simp]

theorem PartENat.dom_one : Part.Dom 1

instance PartENat.instCanLiftNatCastDom : CanLift PartENat ℕ Nat.cast Part.Dom

instance PartENat.instLE : LE PartENat

Equations

• PartENat.instLE = { le := fun (x y : PartENat) => ∃ (h : y.Dom → x.Dom), ∀ (hy : y.Dom), x.get ⋯ ≤ y.get hy }

instance PartENat.instTop : Top PartENat

Equations

• PartENat.instTop = { top := Part.none }

instance PartENat.instBot : Bot PartENat

Equations

• PartENat.instBot = { bot := 0 }

instance PartENat.instMax : Max PartENat

Equations

• PartENat.instMax = { max := fun (x y : PartENat) => { Dom := x.Dom ∧ y.Dom, get := fun (h : x.Dom ∧ y.Dom) => max (x.get ⋯) (y.get ⋯) } }

theorem PartENat.le_def (x y : PartENat) : x ≤ y ↔ ∃ (h : y.Dom → x.Dom), ∀ (hy : y.Dom), x.get ⋯ ≤ y.get hy

theorem PartENat.casesOn' {P : PartENat → Prop} (a : PartENat) : P ⊤ → (∀ (n : ℕ), P ↑n) → P a

theorem PartENat.casesOn {P : PartENat → Prop} (a : PartENat) : P ⊤ → (∀ (n : ℕ), P ↑n) → P a

theorem PartENat.top_add (x : PartENat) : ⊤ + x = ⊤

theorem PartENat.add_top (x : PartENat) : x + ⊤ = ⊤

@[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 y : PartENat} (h : (x + y).Dom) : (x + y).get h = x.get ⋯ + y.get ⋯

@[simp]

theorem PartENat.get_zero (h : Part.Dom 0) : Part.get 0 h = 0

@[simp]

theorem PartENat.get_one (h : Part.Dom 1) : Part.get 1 h = 1

@[simp]

theorem PartENat.get_ofNat' (x : ℕ) [x.AtLeastTwo] (h : (OfNat.ofNat x).Dom) : (OfNat.ofNat x).get h = OfNat.ofNat x

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 y : PartENat} : x ≤ y → y.Dom → x.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 y : PartENat) [Decidable x.Dom] [Decidable y.Dom] : Decidable (x ≤ y)

Equations

• x.decidableLe y = if hx : x.Dom then decidable_of_decidable_of_iff ⋯ else if hy : y.Dom then isFalse ⋯ else isTrue ⋯

instance PartENat.partialOrder : PartialOrder PartENat

Equations

• One or more equations did not get rendered due to their size.

theorem PartENat.lt_def (x y : PartENat) : x < y ↔ ∃ (hx : x.Dom), ∀ (hy : y.Dom), x.get hx < y.get hy

instance PartENat.isOrderedAddMonoid : IsOrderedAddMonoid PartENat

instance PartENat.semilatticeSup : SemilatticeSup PartENat

Equations

• One or more equations did not get rendered due to their size.

instance PartENat.orderBot : OrderBot PartENat

Equations

• PartENat.orderBot = { toBot := PartENat.instBot, bot_le := PartENat.orderBot._proof_1 }

instance PartENat.orderTop : OrderTop PartENat

Equations

• PartENat.orderTop = { toTop := PartENat.instTop, le_top := PartENat.orderTop._proof_1 }

instance PartENat.instZeroLEOneClass : ZeroLEOneClass PartENat

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 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.eq_zero_iff {x : PartENat} : x = 0 ↔ x ≤ 0

theorem PartENat.ne_zero_iff {x : PartENat} : x ≠ 0 ↔ ⊥ < x

theorem PartENat.dom_of_lt {x y : PartENat} : x < y → x.Dom

theorem PartENat.top_eq_none : ⊤ = Part.none

@[simp]

theorem PartENat.natCast_lt_top (x : ℕ) : ↑x < ⊤

@[simp]

theorem PartENat.zero_lt_top : 0 < ⊤

@[simp]

theorem PartENat.one_lt_top : 1 < ⊤

@[simp]

theorem PartENat.ofNat_lt_top (x : ℕ) [x.AtLeastTwo] : OfNat.ofNat x < ⊤

@[simp]

theorem PartENat.natCast_ne_top (x : ℕ) : ↑x ≠ ⊤

@[simp]

theorem PartENat.zero_ne_top : 0 ≠ ⊤

@[simp]

theorem PartENat.one_ne_top : 1 ≠ ⊤

@[simp]

theorem PartENat.ofNat_ne_top (x : ℕ) [x.AtLeastTwo] : OfNat.ofNat x ≠ ⊤

theorem PartENat.not_isMax_natCast (x : ℕ) : ¬IsMax ↑x

theorem PartENat.ne_top_iff {x : PartENat} : x ≠ ⊤ ↔ ∃ (n : ℕ), x = ↑n

theorem PartENat.ne_top_iff_dom {x : PartENat} : x ≠ ⊤ ↔ x.Dom

theorem PartENat.not_dom_iff_eq_top {x : PartENat} : ¬x.Dom ↔ x = ⊤

theorem PartENat.ne_top_of_lt {x y : PartENat} (h : x < y) : x ≠ ⊤

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

theorem PartENat.pos_iff_one_le {x : PartENat} : 0 < x ↔ 1 ≤ x

instance PartENat.isTotal : IsTotal PartENat fun (x1 x2 : PartENat) => x1 ≤ x2

noncomputable instance PartENat.linearOrder : LinearOrder PartENat

Equations

• One or more equations did not get rendered due to their size.

instance PartENat.boundedOrder : BoundedOrder PartENat

Equations

• PartENat.boundedOrder = { toOrderTop := PartENat.orderTop, toOrderBot := PartENat.orderBot }

noncomputable instance PartENat.lattice : Lattice PartENat

Equations

• PartENat.lattice = { toSemilatticeSup := PartENat.semilatticeSup, inf := min, inf_le_left := ⋯, inf_le_right := ⋯, le_inf := ⋯ }

instance PartENat.instCanonicallyOrderedAdd : CanonicallyOrderedAdd PartENat

theorem PartENat.eq_natCast_sub_of_add_eq_natCast {x y : PartENat} {n : ℕ} (h : x + y = ↑n) : x = ↑(n - y.get ⋯)

theorem PartENat.add_lt_add_right {x y z : PartENat} (h : x < y) (hz : z ≠ ⊤) : x + z < y + z

theorem PartENat.add_lt_add_iff_right {x y z : PartENat} (hz : z ≠ ⊤) : x + z < y + z ↔ x < y

theorem PartENat.add_lt_add_iff_left {x y z : PartENat} (hz : z ≠ ⊤) : z + x < z + y ↔ x < y

theorem PartENat.lt_add_iff_pos_right {x 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 y : PartENat} (h : x < y + 1) : x ≤ y

theorem PartENat.add_one_le_of_lt {x y : PartENat} (h : x < y) : x + 1 ≤ y

theorem PartENat.add_one_le_iff_lt {x 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 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_eq_top_iff {a b : PartENat} : a + b = ⊤ ↔ a = ⊤ ∨ b = ⊤

theorem PartENat.add_right_cancel_iff {a b c : PartENat} (hc : c ≠ ⊤) : a + c = b + c ↔ a = b

theorem PartENat.add_left_cancel_iff {a b c : PartENat} (ha : a ≠ ⊤) : a + b = a + c ↔ b = c

def PartENat.toWithTop (x : PartENat) [Decidable x.Dom] : ℕ∞

Computably converts a PartENat to a ℕ∞.

Equations

• x.toWithTop = Part.toOption x

theorem PartENat.toWithTop_top : have this := Part.noneDecidable; ⊤.toWithTop = ⊤

@[simp]

theorem PartENat.toWithTop_top' {h : Decidable ⊤.Dom} : ⊤.toWithTop = ⊤

theorem PartENat.toWithTop_zero : have this := Part.someDecidable 0; toWithTop 0 = 0

@[simp]

theorem PartENat.toWithTop_zero' {h : Decidable (Part.Dom 0)} : toWithTop 0 = 0

theorem PartENat.toWithTop_one : have this := Part.someDecidable 1; toWithTop 1 = 1

@[simp]

theorem PartENat.toWithTop_one' {h : Decidable (Part.Dom 1)} : toWithTop 1 = 1

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 (Part.Dom (OfNat.ofNat n))} : (OfNat.ofNat n).toWithTop = OfNat.ofNat n

@[simp]

theorem PartENat.toWithTop_le {x y : PartENat} [hx : Decidable x.Dom] [hy : Decidable y.Dom] : x.toWithTop ≤ y.toWithTop ↔ x ≤ y

@[simp]

theorem PartENat.toWithTop_lt {x y : PartENat} [Decidable x.Dom] [Decidable y.Dom] : x.toWithTop < y.toWithTop ↔ x < y

def PartENat.ofENat : ℕ∞ → PartENat

Coercion from ℕ∞ to PartENat.

Equations

• ↑none = Part.none
• ↑(some n) = ↑n

instance PartENat.instCoeENat : Coe ℕ∞ PartENat

Equations

• PartENat.instCoeENat = { coe := PartENat.ofENat }

@[simp]

theorem PartENat.ofENat_top : ↑⊤ = ⊤

@[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] : ↑(OfNat.ofNat n) = OfNat.ofNat n

@[simp]

theorem PartENat.toWithTop_ofENat (n : ℕ∞) {x✝ : Decidable (↑n).Dom} : (↑n).toWithTop = n

@[simp]

theorem PartENat.ofENat_toWithTop (x : PartENat) {x✝ : 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 y : PartENat} : (x + y).toWithTop = x.toWithTop + y.toWithTop

noncomputable def PartENat.withTopEquiv : PartENat ≃ ℕ∞

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

Equations

• PartENat.withTopEquiv = { toFun := fun (x : PartENat) => x.toWithTop, invFun := fun (x : ℕ∞) => ↑x, left_inv := PartENat.withTopEquiv._proof_1, right_inv := PartENat.withTopEquiv._proof_2 }

@[simp]

theorem PartENat.withTopEquiv_symm_apply (x : ℕ∞) : withTopEquiv.symm x = ↑x

@[simp]

theorem PartENat.withTopEquiv_apply (x : PartENat) : withTopEquiv x = x.toWithTop

theorem PartENat.withTopEquiv_top : withTopEquiv ⊤ = ⊤

theorem PartENat.withTopEquiv_natCast (n : ℕ) : withTopEquiv ↑n = ↑n

theorem PartENat.withTopEquiv_zero : withTopEquiv 0 = 0

theorem PartENat.withTopEquiv_one : withTopEquiv 1 = 1

theorem PartENat.withTopEquiv_ofNat (n : ℕ) [n.AtLeastTwo] : withTopEquiv (OfNat.ofNat n) = OfNat.ofNat n

theorem PartENat.withTopEquiv_le {x y : PartENat} : withTopEquiv x ≤ withTopEquiv y ↔ x ≤ y

theorem PartENat.withTopEquiv_lt {x y : PartENat} : withTopEquiv x < withTopEquiv y ↔ x < y

theorem PartENat.withTopEquiv_symm_top : withTopEquiv.symm ⊤ = ⊤

theorem PartENat.withTopEquiv_symm_coe (n : ℕ) : withTopEquiv.symm ↑n = ↑n

theorem PartENat.withTopEquiv_symm_zero : withTopEquiv.symm 0 = 0

theorem PartENat.withTopEquiv_symm_one : withTopEquiv.symm 1 = 1

theorem PartENat.withTopEquiv_symm_ofNat (n : ℕ) [n.AtLeastTwo] : withTopEquiv.symm (OfNat.ofNat n) = OfNat.ofNat n

theorem PartENat.withTopEquiv_symm_le {x y : ℕ∞} : withTopEquiv.symm x ≤ withTopEquiv.symm y ↔ x ≤ y

theorem PartENat.withTopEquiv_symm_lt {x y : ℕ∞} : withTopEquiv.symm x < withTopEquiv.symm y ↔ x < y

noncomputable def PartENat.withTopOrderIso : PartENat ≃o ℕ∞

toWithTop induces an order isomorphism between PartENat and ℕ∞.

Equations

• PartENat.withTopOrderIso = { toEquiv := PartENat.withTopEquiv, map_rel_iff' := ⋯ }

noncomputable def PartENat.withTopAddEquiv : PartENat ≃+ ℕ∞

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

Equations

• PartENat.withTopAddEquiv = { toEquiv := PartENat.withTopEquiv, map_add' := PartENat.withTopAddEquiv._proof_1 }

theorem PartENat.lt_wf : WellFounded fun (x1 x2 : PartENat) => x1 < x2

instance PartENat.instWellFoundedLT : WellFoundedLT PartENat

instance PartENat.wellFoundedRelation : WellFoundedRelation PartENat

Equations

• PartENat.wellFoundedRelation = { rel := fun (x1 x2 : PartENat) => x1 < x2, wf := PartENat.lt_wf }

def PartENat.find (P : ℕ → Prop) [DecidablePred P] : PartENat

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

Equations

• PartENat.find P = { Dom := ∃ (n : ℕ), P n, get := Nat.find }

@[simp]

theorem PartENat.find_get (P : ℕ → Prop) [DecidablePred P] (h : (find P).Dom) : (find P).get h = Nat.find h

theorem PartENat.find_dom (P : ℕ → Prop) [DecidablePred P] (h : ∃ (n : ℕ), P n) : (find P).Dom

theorem PartENat.lt_find (P : ℕ → Prop) [DecidablePred P] (n : ℕ) (h : ∀ m ≤ n, ¬P m) : ↑n < find P

theorem PartENat.lt_find_iff (P : ℕ → Prop) [DecidablePred P] (n : ℕ) : ↑n < find P ↔ ∀ m ≤ n, ¬P m

theorem PartENat.find_le (P : ℕ → Prop) [DecidablePred P] (n : ℕ) (h : P n) : find P ≤ ↑n

theorem PartENat.find_eq_top_iff (P : ℕ → Prop) [DecidablePred P] : find P = ⊤ ↔ ∀ (n : ℕ), ¬P n

noncomputable instance PartENat.instLinearOrderedAddCommMonoidWithTop : LinearOrderedAddCommMonoidWithTop PartENat

Equations

• One or more equations did not get rendered due to their size.

noncomputable instance PartENat.instCompleteLinearOrder : CompleteLinearOrder PartENat

Equations

• One or more equations did not get rendered due to their size.