Definition and notation for extended natural numbers

def ENat : Type

Extended natural numbers ℕ∞ = WithTop ℕ.

Equations

• ℕ∞ = WithTop ℕ

Instances For

• Cardinal.instCanLiftENatOfENatLeAleph0
• Cardinal.instCoeENat
• ENat.canLift
• ENat.instCanonicallyOrderedAdd
• ENat.instCharZero
• ENat.instCountable
• ENat.instIsOrderedRing
• ENat.instNatCast
• ENat.instNoZeroDivisors
• ENat.instOrderBot
• ENat.instOrderTop
• ENat.instOrderedSub
• ENat.instSuccAddOrder
• ENat.instSuccOrder
• ENat.instWellFoundedLT
• ENat.instWellFoundedRelation
• instENatBot
• instENatCommSemiring
• instENatInhabited
• instENatLinearOrder
• instENatLinearOrderedAddCommMonoidWithTop
• instENatNontrivial
• instENatSub
• instENatTop
• instENatWellFoundedRelation
• instENatZero

instance instENatTop : Top ℕ∞

Equations

• instENatTop = WithTop.top

instance instENatInhabited : Inhabited ℕ∞

Equations

• instENatInhabited = WithTop.inhabited

def «termℕ∞» : Lean.ParserDescr

Extended natural numbers ℕ∞ = WithTop ℕ.

Equations

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

instance ENat.instNatCast : NatCast ℕ∞

Equations

• ENat.instNatCast = { natCast := WithTop.some }

def ENat.recTopCoe {C : ℕ∞ → Sort u_1} (top : C ⊤) (coe : (a : ℕ) → C ↑a) (n : ℕ∞) : C n

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

Equations

• ENat.recTopCoe top coe none = top
• ENat.recTopCoe top coe (some a) = coe a

@[simp]

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

@[simp]

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