Documentation

Mathlib.Data.ENat.Defs

Definition and notation for extended natural numbers #

source
def ENat :
Type

Extended natural numbers ℕ∞ = WithTop ℕ.

Instances For
    source
    @[instance_reducible]
    instance instTopENat :
    Top ℕ∞
    source
    @[instance_reducible]
    instance instInhabitedENat :
    Inhabited ℕ∞
    source
    def «termℕ∞» :
    Lean.ParserDescr

    Extended natural numbers ℕ∞ = WithTop ℕ.

    Instances For
      source
      @[instance_reducible]
      instance ENat.instNatCast :
      NatCast ℕ∞
      source
      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.

      Instances For
        source
        @[simp]
        theorem ENat.recTopCoe_top {C : ℕ∞ → Sort u_1} (d : C ⊤) (f : (a : ℕ) → C ↑a) :
        recTopCoe d f ⊤ = d
        source
        @[simp]
        theorem ENat.recTopCoe_natCast {C : ℕ∞ → Sort u_1} (d : C ⊤) (f : (a : ℕ) → C ↑a) (x : ℕ) :
        recTopCoe d f ↑x = f x
        source
        @[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.