Definition and basic properties of extended natural numbers #

In this file we define ENat (notation: ℕ∞∞) to be WithTop ℕ and prove some basic lemmas about this type.

source

ink

def ENat :

Type

Extended natural numbers ℕ∞ = WithTop ℕ∞ = WithTop ℕ.

Equations

ℕ∞ = WithTop ℕ

source

ink

def «termℕ∞» :

Lean.ParserDescr

Extended natural numbers ℕ∞ = WithTop ℕ∞ = WithTop ℕ.

Equations

«termℕ∞» = Lean.ParserDescr.node `termℕ∞ 1024 (Lean.ParserDescr.symbol "ℕ∞")

source

ink

instance ENat.instOrderBotENatToLEToPreorderToPartialOrderToOrderedSemiringToOrderedCommSemiringInstENatCanonicallyOrderedCommSemiring :

OrderBot ℕ∞

Equations

ENat.instOrderBotENatToLEToPreorderToPartialOrderToOrderedSemiringToOrderedCommSemiringInstENatCanonicallyOrderedCommSemiring = WithTop.orderBot

source

ink

instance ENat.instOrderTopENatToLEToPreorderToPartialOrderToOrderedSemiringToOrderedCommSemiringInstENatCanonicallyOrderedCommSemiring :

OrderTop ℕ∞

Equations

ENat.instOrderTopENatToLEToPreorderToPartialOrderToOrderedSemiringToOrderedCommSemiringInstENatCanonicallyOrderedCommSemiring = WithTop.orderTop

source

ink

instance ENat.instOrderedSubENatToLEToPreorderToPartialOrderToOrderedSemiringToOrderedCommSemiringInstENatCanonicallyOrderedCommSemiringToAddToDistribToNonUnitalNonAssocSemiringToNonAssocSemiringToSemiringInstENatSub :

OrderedSub ℕ∞

Equations

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

source

ink

instance ENat.instSuccOrderENatToPreorderToPartialOrderToOrderedSemiringToOrderedCommSemiringInstENatCanonicallyOrderedCommSemiring :

SuccOrder ℕ∞

Equations

ENat.instSuccOrderENatToPreorderToPartialOrderToOrderedSemiringToOrderedCommSemiringInstENatCanonicallyOrderedCommSemiring = inferInstanceAs (SuccOrder (WithTop ℕ))

source

ink

instance ENat.instWellFoundedLTENatToLTToPreorderToPartialOrderToOrderedSemiringToOrderedCommSemiringInstENatCanonicallyOrderedCommSemiring :

WellFoundedLT ℕ∞

Equations

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

source

ink

instance ENat.instCharZeroENatToAddMonoidWithOneToAddCommMonoidWithOneToNonAssocSemiringToSemiringToOrderedSemiringToOrderedCommSemiringInstENatCanonicallyOrderedCommSemiring :

CharZero ℕ∞

Equations

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

source

ink

instance ENat.instIsWellOrderENatLtToLTToPreorderToPartialOrderToOrderedSemiringToOrderedCommSemiringInstENatCanonicallyOrderedCommSemiring :

IsWellOrder ℕ∞ fun x x_1 => x < x_1

Equations

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

source

ink

theorem ENat.coe_zero :

↑0 = 0

source

ink

theorem ENat.coe_one :

↑1 = 1

source

ink

theorem ENat.coe_add (m : ℕ) (n : ℕ) :

↑(m + n) = ↑m + ↑n

source

ink

@[simp]

theorem ENat.coe_sub (m : ℕ) (n : ℕ) :

↑(m - n) = ↑m - ↑n

source

ink

theorem ENat.coe_mul (m : ℕ) (n : ℕ) :

↑(m * n) = ↑m * ↑n

source

ink

instance ENat.canLift :

CanLift ℕ∞ ℕ Nat.cast fun n => n ≠ ⊤

Equations

ENat.canLift = WithTop.canLift

source

ink

def ENat.toNat :

ℕ∞ →*₀ ℕ

Conversion of ℕ∞∞ to ℕ sending ∞∞ to 0.

Equations

ENat.toNat = { toZeroHom := { toFun := WithTop.untop' 0, map_zero' := ENat.toNat.proof_1 }, map_one' := ENat.toNat.proof_2, map_mul' := ENat.toNat.proof_3 }

source

ink

@[simp]

theorem ENat.toNat_coe (n : ℕ) :

↑ENat.toNat ↑n = n

source

ink

@[simp]

theorem ENat.toNat_top :

↑ENat.toNat ⊤ = 0

source

ink

def ENat.recTopCoe {C : ℕ∞ → Sort u_1} (h₁ : C ⊤) (h₂ : (a : ℕ) → C ↑a) (n : ℕ∞) :

C n

Recursor for ENat using the preferred forms ⊤⊤ and ↑a↑a.

Equations

ENat.recTopCoe h₁ h₂ x = match x with | none => h₁ | some a => h₂ a

source

ink

@[simp]

theorem ENat.recTopCoe_top {C : ℕ∞ → Sort u_1} (d : C ⊤) (f : (a : ℕ) → C ↑a) :

ENat.recTopCoe d f ⊤ = d

source

ink

@[simp]

theorem ENat.recTopCoe_coe {C : ℕ∞ → Sort u_1} (d : C ⊤) (f : (a : ℕ) → C ↑a) (x : ℕ) :

ENat.recTopCoe d f ↑x = f x

source

ink

@[simp]

theorem ENat.top_ne_coe (a : ℕ) :

⊤ ≠ ↑a

source

ink

@[simp]

theorem ENat.coe_ne_top (a : ℕ) :

↑a ≠ ⊤

source

ink

@[simp]

theorem ENat.top_sub_coe (a : ℕ) :

⊤ - ↑a = ⊤

source

ink

theorem ENat.sub_top (a : ℕ∞) :

a - ⊤ = 0

source

ink

@[simp]

theorem ENat.coe_toNat_eq_self {n : ℕ∞} :

↑(↑ENat.toNat n) = n ↔ n ≠ ⊤

source

ink

theorem ENat.coe_toNat {n : ℕ∞} :

n ≠ ⊤ → ↑(↑ENat.toNat n) = n

Alias of the reverse direction of ENat.coe_toNat_eq_self.

source

ink

theorem ENat.coe_toNat_le_self (n : ℕ∞) :

↑(↑ENat.toNat n) ≤ n

source

ink

theorem ENat.toNat_add {m : ℕ∞} {n : ℕ∞} (hm : m ≠ ⊤) (hn : n ≠ ⊤) :

↑ENat.toNat (m + n) = ↑ENat.toNat m + ↑ENat.toNat n

source

ink

theorem ENat.toNat_sub {n : ℕ∞} (hn : n ≠ ⊤) (m : ℕ∞) :

↑ENat.toNat (m - n) = ↑ENat.toNat m - ↑ENat.toNat n

source

ink

theorem ENat.toNat_eq_iff {m : ℕ∞} {n : ℕ} (hn : n ≠ 0) :

↑ENat.toNat m = n ↔ m = ↑n

source

ink

@[simp]

theorem ENat.succ_def (m : ℕ∞) :

Order.succ m = m + 1

source

ink

theorem ENat.add_one_le_of_lt {m : ℕ∞} {n : ℕ∞} (h : m < n) :

m + 1 ≤ n

source

ink

theorem ENat.add_one_le_iff {m : ℕ∞} {n : ℕ∞} (hm : m ≠ ⊤) :

m + 1 ≤ n ↔ m < n

source

ink

theorem ENat.one_le_iff_pos {n : ℕ∞} :

1 ≤ n ↔ 0 < n

source

ink

theorem ENat.one_le_iff_ne_zero {n : ℕ∞} :

1 ≤ n ↔ n ≠ 0

source

ink

theorem ENat.le_of_lt_add_one {m : ℕ∞} {n : ℕ∞} (h : m < n + 1) :

m ≤ n

source

ink

theorem ENat.nat_induction {P : ℕ∞ → Prop} (a : ℕ∞) (h0 : P 0) (hsuc : (n : ℕ) → P ↑n → P ↑(Nat.succ n)) (htop : ((n : ℕ) → P ↑n) → P ⊤) :

P a