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:

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

def PartENat.some :

ℕ → PartENat

The computable embedding ℕ → PartENat.

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

Instances For

instance PartENat.instZeroPartENat :

instance PartENat.instInhabitedPartENat :

Inhabited PartENat

instance PartENat.instOnePartENat :

instance PartENat.instAddPartENat :

instance PartENat.instDecidableDomNatSome (n : ℕ) :

Decidable (↑n).Dom

@[simp]

theorem PartENat.dom_some (x : ℕ) :

(↑x).Dom

instance PartENat.addCommMonoid :

AddCommMonoid PartENat

instance PartENat.instAddCommMonoidWithOnePartENat :

AddCommMonoidWithOne PartENat

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

instance PartENat.instCanLiftPartENatNatCastToNatCastToAddMonoidWithOneInstAddCommMonoidWithOnePartENatDom :

CanLift PartENat ℕ Nat.cast Part.Dom

instance PartENat.instLEPartENat :

instance PartENat.instTopPartENat :

instance PartENat.instBotPartENat :

instance PartENat.instSupPartENat :

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

theorem PartENat.add_top (x : PartENat) :

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

Decidable (x ≤ y)

def PartENat.natCast_AddMonoidHom :

ℕ →+ PartENat

The coercion ℕ → PartENat preserves 0 and addition.

Instances For

@[simp]

theorem PartENat.coe_coeHom :

↑PartENat.natCast_AddMonoidHom = PartENat.some

instance PartENat.partialOrder :

PartialOrder PartENat

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

instance PartENat.NeZero.one :

instance PartENat.semilatticeSup :

SemilatticeSup PartENat

instance PartENat.orderBot :

OrderBot PartENat

instance PartENat.orderTop :

OrderTop PartENat

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 : PartENat} {y : PartENat} :

x < y → x.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.not_isMax_natCast (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 : 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

theorem PartENat.pos_iff_one_le {x : PartENat} :

0 < x ↔ 1 ≤ x

instance PartENat.isTotal :

IsTotal PartENat fun x x_1 => x ≤ x_1

noncomputable instance PartENat.linearOrder :

LinearOrder PartENat

instance PartENat.boundedOrder :

BoundedOrder PartENat

noncomputable instance PartENat.lattice :

Lattice PartENat

noncomputable instance PartENat.orderedAddCommMonoid :

OrderedAddCommMonoid PartENat

noncomputable instance PartENat.instCanonicallyOrderedAddMonoidPartENat :

CanonicallyOrderedAddMonoid PartENat

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

↑(Nat.succ n) ≤ 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 < ↑(Nat.succ n) ↔ x ≤ ↑n

theorem PartENat.add_eq_top_iff {a : PartENat} {b : PartENat} :

a + b = ⊤ ↔ a = ⊤ ∨ b = ⊤

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

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

Computably converts a PartENat to a ℕ∞.

Instances For

theorem PartENat.toWithTop_top :

let_fun this := Part.noneDecidable; PartENat.toWithTop ⊤ = ⊤

@[simp]

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

PartENat.toWithTop ⊤ = ⊤

theorem PartENat.toWithTop_zero :

let_fun this := Part.someDecidable 0; PartENat.toWithTop 0 = 0

@[simp]

theorem PartENat.toWithTop_zero' {h : Decidable 0.Dom} :

PartENat.toWithTop 0 = 0

theorem PartENat.toWithTop_some (n : ℕ) :

PartENat.toWithTop ↑n = ↑n

theorem PartENat.toWithTop_natCast (n : ℕ) :

∀ {x : Decidable (↑n).Dom}, PartENat.toWithTop ↑n = ↑n

@[simp]

theorem PartENat.toWithTop_natCast' (n : ℕ) {h : Decidable (↑n).Dom} :

PartENat.toWithTop ↑n = ↑n

@[simp]

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

PartENat.toWithTop x ≤ PartENat.toWithTop y ↔ x ≤ y

@[simp]

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

PartENat.toWithTop x < PartENat.toWithTop y ↔ x < y

def PartENat.ofENat :

ℕ∞ → PartENat

Coercion from ℕ∞ to PartENat.

Instances For

instance PartENat.instCoeENatPartENat :

Coe ℕ∞ PartENat

@[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}, PartENat.toWithTop ↑n = n

@[simp]

theorem PartENat.toWithTop_add {x : PartENat} {y : PartENat} :

PartENat.toWithTop (x + y) = PartENat.toWithTop x + PartENat.toWithTop y

noncomputable def PartENat.withTopEquiv :

PartENat ≃ ℕ∞

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

Instances For

@[simp]

theorem PartENat.withTopEquiv_top :

↑PartENat.withTopEquiv ⊤ = ⊤

@[simp]

theorem PartENat.withTopEquiv_natCast (n : ℕ) :

↑PartENat.withTopEquiv ↑n = ↑n

@[simp]

theorem PartENat.withTopEquiv_zero :

↑PartENat.withTopEquiv 0 = 0

@[simp]

theorem PartENat.withTopEquiv_le {x : PartENat} {y : PartENat} :

↑PartENat.withTopEquiv x ≤ ↑PartENat.withTopEquiv y ↔ x ≤ y

@[simp]

theorem PartENat.withTopEquiv_lt {x : PartENat} {y : PartENat} :

↑PartENat.withTopEquiv x < ↑PartENat.withTopEquiv y ↔ x < y

noncomputable def PartENat.withTopOrderIso :

PartENat ≃o ℕ∞

to_WithTop induces an order isomorphism between PartENat and ℕ∞.

Instances For

@[simp]

theorem PartENat.withTopEquiv_symm_top :

↑PartENat.withTopEquiv.symm ⊤ = ⊤

@[simp]

theorem PartENat.withTopEquiv_symm_coe (n : ℕ) :

↑PartENat.withTopEquiv.symm ↑n = ↑n

@[simp]

theorem PartENat.withTopEquiv_symm_zero :

↑PartENat.withTopEquiv.symm 0 = 0

@[simp]

theorem PartENat.withTopEquiv_symm_le {x : ℕ∞} {y : ℕ∞} :

↑PartENat.withTopEquiv.symm x ≤ ↑PartENat.withTopEquiv.symm y ↔ x ≤ y

@[simp]

theorem PartENat.withTopEquiv_symm_lt {x : ℕ∞} {y : ℕ∞} :

↑PartENat.withTopEquiv.symm x < ↑PartENat.withTopEquiv.symm y ↔ x < y

noncomputable def PartENat.withTopAddEquiv :

PartENat ≃+ ℕ∞

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.instWellFoundedLTPartENatToLTToPreorderPartialOrder :

WellFoundedLT PartENat

instance PartENat.isWellOrder :

IsWellOrder PartENat fun x x_1 => x < x_1

instance PartENat.wellFoundedRelation :

WellFoundedRelation PartENat

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

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

Instances For

@[simp]

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

Part.get (PartENat.find P) h = Nat.find h

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

(PartENat.find P).Dom

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

↑n < PartENat.find P

theorem PartENat.lt_find_iff (P : ℕ → Prop) [DecidablePred P] (n : ℕ) :

↑n < PartENat.find P ↔ ∀ (m : ℕ), m ≤ n → ¬P m

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

PartENat.find P ≤ ↑n

theorem PartENat.find_eq_top_iff (P : ℕ → Prop) [DecidablePred P] :

PartENat.find P = ⊤ ↔ ∀ (n : ℕ), ¬P n

noncomputable instance PartENat.instLinearOrderedAddCommMonoidWithTopPartENat :

LinearOrderedAddCommMonoidWithTop PartENat

noncomputable instance PartENat.instCompleteLinearOrderPartENat :

CompleteLinearOrder PartENat