Definition and notation for extended natural numbers

def ENat : Type

Extended natural numbers ℕ∞ = WithTop ℕ.

@[implicit_reducible]

instance instTopENat : Top ℕ∞

@[implicit_reducible]

instance instInhabitedENat : Inhabited ℕ∞

def «termℕ∞» : Lean.ParserDescr

Extended natural numbers ℕ∞ = WithTop ℕ.

@[implicit_reducible]

instance ENat.instNatCast : NatCast ℕ∞

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.

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