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 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, ℕ∞

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.instZeroPartENat : Zero PartENat

Equations

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

instance PartENat.instInhabitedPartENat : Inhabited PartENat

Equations

• PartENat.instInhabitedPartENat = { default := 0 }

instance PartENat.instOnePartENat : One PartENat

Equations

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

instance PartENat.instAddPartENat : Add PartENat

Equations

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

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

• PartENat.addCommMonoid = AddCommMonoid.mk PartENat.addCommMonoid.proof_6

instance PartENat.instAddCommMonoidWithOnePartENat : AddCommMonoidWithOne PartENat

Equations

• PartENat.instAddCommMonoidWithOnePartENat = let src := PartENat.addCommMonoid; AddCommMonoidWithOne.mk (_ : ∀ (a b : PartENat), a + b = b + a)

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

instance PartENat.instCharZeroPartENatToAddMonoidWithOneInstAddCommMonoidWithOnePartENat : CharZero PartENat

Equations

• PartENat.instCharZeroPartENatToAddMonoidWithOneInstAddCommMonoidWithOnePartENat = (_ : 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 : ℕ) [Nat.AtLeastTwo x] : (OfNat.ofNat x).Dom

@[simp]

theorem PartENat.dom_zero : 0.Dom

@[simp]

theorem PartENat.dom_one : 1.Dom

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

Equations

• PartENat.instCanLiftPartENatNatCastToNatCastToAddMonoidWithOneInstAddCommMonoidWithOnePartENatDom = (_ : CanLift PartENat ℕ Nat.cast Part.Dom)

instance PartENat.instLEPartENat : LE PartENat

Equations

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

instance PartENat.instTopPartENat : Top PartENat

Equations

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

instance PartENat.instBotPartENat : Bot PartENat

Equations

• PartENat.instBotPartENat = { bot := 0 }

instance PartENat.instSupPartENat : Sup PartENat

Equations

• PartENat.instSupPartENat = { sup := fun (x y : PartENat) => { Dom := x.Dom ∧ y.Dom, get := fun (h : x.Dom ∧ y.Dom) => x.get (_ : x.Dom) ⊔ y.get (_ : y.Dom) } }

theorem PartENat.le_def (x : PartENat) (y : PartENat) : x ≤ y ↔ ∃ (h : y.Dom → x.Dom), ∀ (hy : y.Dom), x.get (_ : x.Dom) ≤ 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).Dom) = x

theorem PartENat.coe_add_get {x : ℕ} {y : PartENat} (h : (↑x + y).Dom) : (↑x + y).get h = x + y.get (_ : y.Dom)

@[simp]

theorem PartENat.get_add {x : PartENat} {y : PartENat} (h : (x + y).Dom) : (x + y).get h = x.get (_ : x.Dom) + y.get (_ : y.Dom)

@[simp]

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

@[simp]

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

@[simp]

theorem PartENat.get_ofNat' (x : ℕ) [Nat.AtLeastTwo x] (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 : 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)

Equations

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

instance PartENat.partialOrder : PartialOrder PartENat

Equations

• PartENat.partialOrder = PartialOrder.mk PartENat.partialOrder.proof_4

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

noncomputable instance PartENat.orderedAddCommMonoid : OrderedAddCommMonoid PartENat

Equations

• PartENat.orderedAddCommMonoid = let src := PartENat.partialOrder; let src_1 := PartENat.addCommMonoid; OrderedAddCommMonoid.mk PartENat.orderedAddCommMonoid.proof_1

instance PartENat.semilatticeSup : SemilatticeSup PartENat

Equations

• PartENat.semilatticeSup = let src := PartENat.partialOrder; SemilatticeSup.mk PartENat.semilatticeSup.proof_1 PartENat.semilatticeSup.proof_2 PartENat.semilatticeSup.proof_3

instance PartENat.orderBot : OrderBot PartENat

Equations

• PartENat.orderBot = OrderBot.mk PartENat.orderBot.proof_1

instance PartENat.orderTop : OrderTop PartENat

Equations

• PartENat.orderTop = OrderTop.mk PartENat.orderTop.proof_1

instance PartENat.instZeroLEOneClassPartENatInstZeroPartENatInstOnePartENatInstLEPartENat : ZeroLEOneClass PartENat

Equations

• PartENat.instZeroLEOneClassPartENatInstZeroPartENatInstOnePartENatInstLEPartENat = (_ : 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 : 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.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.zero_lt_top : 0 < ⊤

@[simp]

theorem PartENat.one_lt_top : 1 < ⊤

@[simp]

theorem PartENat.ofNat_lt_top (x : ℕ) [Nat.AtLeastTwo x] : 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 : ℕ) [Nat.AtLeastTwo x] : 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 : PartENat} {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 (x x_1 : PartENat) => x ≤ x_1

Equations

• PartENat.isTotal = (_ : IsTotal PartENat fun (x x_1 : PartENat) => x ≤ x_1)

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 = let src := PartENat.orderTop; let src_1 := PartENat.orderBot; BoundedOrder.mk

noncomputable instance PartENat.lattice : Lattice PartENat

Equations

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

noncomputable instance PartENat.instCanonicallyOrderedAddCommMonoidPartENat : CanonicallyOrderedAddCommMonoid PartENat

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 (_ : 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 ℕ∞.

Equations

• PartENat.toWithTop x = Part.toOption x

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_one : let_fun this := Part.someDecidable 1; PartENat.toWithTop 1 = 1

@[simp]

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

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 : ℕ) : ∀ {x : Decidable (↑n).Dom}, PartENat.toWithTop ↑n = ↑n

@[simp]

theorem PartENat.toWithTop_ofNat (n : ℕ) [Nat.AtLeastTwo n] : ∀ {x : Decidable (OfNat.ofNat n).Dom}, PartENat.toWithTop (OfNat.ofNat n) = OfNat.ofNat 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.

Equations

• ↑x = match x with | none => Part.none | some n => ↑n

instance PartENat.instCoeENatPartENat : Coe ℕ∞ PartENat

Equations

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

@[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).

Equations

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

@[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_one : PartENat.withTopEquiv 1 = 1

@[simp]

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

@[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 ℕ∞.

Equations

• PartENat.withTopOrderIso = let src := PartENat.withTopEquiv; { toEquiv := src, map_rel_iff' := (_ : ∀ (x x_1 : PartENat), PartENat.withTopEquiv x ≤ PartENat.withTopEquiv x_1 ↔ x ≤ x_1) }

@[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_one : PartENat.withTopEquiv.symm 1 = 1

@[simp]

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

@[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 ℕ∞.

Equations

• PartENat.withTopAddEquiv = let src := PartENat.withTopEquiv; { toEquiv := src, map_add' := PartENat.withTopAddEquiv.proof_1 }

theorem PartENat.lt_wf : WellFounded fun (x x_1 : PartENat) => x < x_1

instance PartENat.instWellFoundedLTPartENatToLTToPreorderPartialOrder : WellFoundedLT PartENat

Equations

• PartENat.instWellFoundedLTPartENatToLTToPreorderPartialOrder = (_ : IsWellFounded PartENat fun (x x_1 : PartENat) => x < x_1)

instance PartENat.isWellOrder : IsWellOrder PartENat fun (x x_1 : PartENat) => x < x_1

Equations

• PartENat.isWellOrder = (_ : IsWellOrder PartENat fun (x x_1 : PartENat) => x < x_1)

instance PartENat.wellFoundedRelation : WellFoundedRelation PartENat

Equations

• PartENat.wellFoundedRelation = { rel := fun (x x_1 : PartENat) => x < x_1, 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 : (PartENat.find P).Dom) : (PartENat.find P).get 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 ≤ n, ¬P m) : ↑n < PartENat.find P

theorem PartENat.lt_find_iff (P : ℕ → Prop) [DecidablePred P] (n : ℕ) : ↑n < PartENat.find P ↔ ∀ 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

Equations

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

noncomputable instance PartENat.instCompleteLinearOrderPartENat : CompleteLinearOrder PartENat

Equations

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