Documentation

Mathlib.Data.ENat.Defs

Definition and notation for extended natural numbers #

def ENat :

Extended natural numbers ℕ∞ = WithTop.

Equations
    Instances For
      Equations

        Extended natural numbers ℕ∞ = WithTop.

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