Definition and notation for extended natural numbers

def ENat : Type

Extended natural numbers ℕ∞ = WithTop ℕ.

Equations

• ℕ∞ = WithTop ℕ

@[instance_reducible]

instance instTopENat : Top ℕ∞

Equations

• instTopENat = { top := instTopENat._aux_1 }

@[instance_reducible]

instance instInhabitedENat : Inhabited ℕ∞

Equations

• instInhabitedENat = { default := instInhabitedENat._aux_1 }

def «termℕ∞» : Lean.ParserDescr

Extended natural numbers ℕ∞ = WithTop ℕ.

Equations

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

@[instance_reducible]

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_natCast {C : ℕ∞ → Sort u_1} (d : C ⊤) (f : (a : ℕ) → C ↑a) (x : ℕ) : recTopCoe d f ↑x = f x

@[deprecated ENat.recTopCoe_natCast (since := "2026-07-17")]

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

Alias of ENat.recTopCoe_natCast.