Mathlib.Data.ENat.Defs

ENat definition

: Type

Full source

/-- Extended natural numbers `ℕ∞ = WithTop ℕ`. -/
def ENat : Type := WithTop ℕ deriving Top, Inhabited

Extended natural numbers

Informal description

The type of extended natural numbers, denoted as $\mathbb{N}_\infty$, is defined as the natural numbers $\mathbb{N}$ with an additional element $\infty$ adjoined (using the `WithTop` construction).

termℕ∞ definition

: Lean.ParserDescr✝

Full source

@[inherit_doc] notation "ℕ∞" => ENat

Notation for extended natural numbers

Informal description

The notation `ℕ∞` is defined as an alias for the type `ENat`, representing the extended natural numbers (natural numbers with infinity).

ENat.instNatCast instance

: NatCast ℕ∞

Full source

instance instNatCast : NatCast ℕ∞ := ⟨WithTop.some⟩

Natural Number Cast into Extended Natural Numbers

Informal description

The extended natural numbers $\mathbb{N}_\infty$ have a canonical way to cast natural numbers into $\mathbb{N}_\infty$.

ENat.recTopCoe definition

{C : ℕ∞ → Sort*} (top : C ⊤) (coe : ∀ a : ℕ, C a) : ∀ n : ℕ∞, C n

Full source

/-- Recursor for `ENat` using the preferred forms `⊤` and `↑a`. -/
@[elab_as_elim, induction_eliminator, cases_eliminator]
def recTopCoe {C : ℕ∞ → Sort*} (top : C ⊤) (coe : ∀ a : ℕ, C a) : ∀ n : ℕ∞, C n
  | none => top
  | Option.someOption.some a => coe a

Recursor for extended natural numbers

Informal description

The recursor for extended natural numbers $\mathbb{N}_\infty$ takes a value `top` of type $C(\infty)$ and a function `coe` mapping each natural number $a$ to a value in $C(a)$, and returns a function that maps any extended natural number $n$ to a value in $C(n)$. For $\infty$, it returns `top`, and for a natural number $a$ lifted to $\mathbb{N}_\infty$, it applies `coe` to $a$.

ENat.recTopCoe_top theorem

{C : ℕ∞ → Sort*} (d : C ⊤) (f : ∀ a : ℕ, C a) : @recTopCoe C d f ⊤ = d

Full source

@[simp]
theorem recTopCoe_top {C : ℕ∞ → Sort*} (d : C ⊤) (f : ∀ a : ℕ, C a) :
    @recTopCoe C d f ⊤ = d :=
  rfl

Recursor Computation Rule for Infinity in Extended Naturals

Informal description

For any type family $C : \mathbb{N}_\infty \to \text{Sort}^*$, given a term $d : C(\infty)$ and a function $f : \forall a \in \mathbb{N}, C(a)$, the recursor $\text{recTopCoe}$ satisfies $\text{recTopCoe}\,d\,f\,\infty = d$.

ENat.recTopCoe_coe theorem

{C : ℕ∞ → Sort*} (d : C ⊤) (f : ∀ a : ℕ, C a) (x : ℕ) : @recTopCoe C d f ↑x = f x

Full source

@[simp]
theorem recTopCoe_coe {C : ℕ∞ → Sort*} (d : C ⊤) (f : ∀ a : ℕ, C a) (x : ℕ) :
    @recTopCoe C d f ↑x = f x :=
  rfl

Recursor Computation Rule for Natural Numbers in Extended Naturals

Informal description

For any type family $C : \mathbb{N}_\infty \to \text{Sort}^*$, given a term $d : C(\infty)$ and a function $f : \forall a \in \mathbb{N}, C(a)$, the recursor $\text{recTopCoe}$ satisfies $\text{recTopCoe}\,d\,f\,(x) = f(x)$ for any natural number $x$ lifted to $\mathbb{N}_\infty$.