doc-next-gen

Mathlib.Data.ENat.Basic

Module docstring

{"# Definition and basic properties of extended natural numbers

In this file we define ENat (notation: ℕ∞) to be WithTop ℕ and prove some basic lemmas about this type.

Implementation details

There are two natural coercions from ℕ to WithTop ℕ = ENat: WithTop.some and Nat.cast. In Lean 3, this difference was hidden in typeclass instances. Since these instances were definitionally equal, we did not duplicate generic lemmas about WithTop α and WithTop.some coercion for ENat and Nat.cast coercion. If you need to apply a lemma about WithTop, you may either rewrite back and forth using ENat.some_eq_coe, or restate the lemma for ENat.

TODO

Unify ENat.add_iSup/ENat.iSup_add with ENNReal.add_iSup/ENNReal.iSup_add. The key property of ENat and ENNReal we are using is that all a are either absorbing for addition (a + b = a for all b), or that it's order-cancellable (a + b ≤ a + c → b ≤ c for all b, c), and similarly for multiplication. "}

ENat.instIsOrderedRing instance
: IsOrderedRing ℕ∞
Full source 
instance : IsOrderedRing ℕ∞ := WithTop.instIsOrderedRing
Extended Natural Numbers as an Ordered Ring
Informal description
The extended natural numbers $\mathbb{N}_\infty$ form an ordered ring.
ENat.instCanonicallyOrderedAdd instance
: CanonicallyOrderedAdd ℕ∞
Full source 
instance : CanonicallyOrderedAdd ℕ∞ := WithTop.canonicallyOrderedAdd
Extended Natural Numbers as a Canonically Ordered Additive Monoid
Informal description
The extended natural numbers $\mathbb{N}_\infty$ form a canonically ordered additive monoid.
ENat.instOrderBot instance
: OrderBot ℕ∞
Full source 
instance : OrderBot ℕ∞ := WithTop.orderBot
Extended Natural Numbers with Bottom Element
Informal description
The extended natural numbers $\mathbb{N}_\infty$ form an ordered set with a least element $0$, where $0$ is less than or equal to all other elements in $\mathbb{N}_\infty$.
ENat.instOrderTop instance
: OrderTop ℕ∞
Full source 
instance : OrderTop ℕ∞ := WithTop.orderTop
Extended Natural Numbers with Top Element
Informal description
The extended natural numbers $\mathbb{N}_\infty$ form an ordered set with a greatest element $\infty$, where $\infty$ is greater than or equal to all other elements in $\mathbb{N}_\infty$.
ENat.instOrderedSub instance
: OrderedSub ℕ∞
Full source 
instance : OrderedSub ℕ∞ := inferInstanceAs (OrderedSub (WithTop ℕ))
Ordered Subtraction on Extended Natural Numbers
Informal description
The extended natural numbers $\mathbb{N}_\infty$ form an ordered structure where subtraction is compatible with the order, meaning that for any $a, b, c \in \mathbb{N}_\infty$, the inequality $a - b \leq c$ holds if and only if $a \leq b + c$.
ENat.instSuccOrder instance
: SuccOrder ℕ∞
Full source 
instance : SuccOrder ℕ∞ := inferInstanceAs (SuccOrder (WithTop ℕ))
Successor Order Structure on Extended Natural Numbers
Informal description
The extended natural numbers $\mathbb{N}_\infty$ form a successor order, where the successor operation is defined in the usual way on $\mathbb{N}$ and $\infty$ is its own successor.
ENat.instWellFoundedLT instance
: WellFoundedLT ℕ∞
Full source 
instance : WellFoundedLT ℕ∞ := inferInstanceAs (WellFoundedLT (WithTop ℕ))
Well-foundedness of Extended Natural Numbers under Less-Than Relation
Informal description
The extended natural numbers $\mathbb{N}_\infty$ are well-founded with respect to the less-than relation.
ENat.instCharZero instance
: CharZero ℕ∞
Full source 
instance : CharZero ℕ∞ := inferInstanceAs (CharZero (WithTop ℕ))
Characteristic Zero Property of Extended Natural Numbers
Informal description
The extended natural numbers $\mathbb{N}_\infty$ have characteristic zero, meaning the canonical embedding of natural numbers into $\mathbb{N}_\infty$ is injective.
ENat.some_eq_coe theorem
: (WithTop.some : ℕ → ℕ∞) = Nat.cast
Full source 
/-- Lemmas about `WithTop` expect (and can output) `WithTop.some` but the normal form for coercion
`ℕ → ℕ∞` is `Nat.cast`. -/
@[simp] theorem some_eq_coe : (WithTop.some : ℕ → ℕ∞) = Nat.cast := rfl
Equality of `WithTop.some` and `Nat.cast` for Extended Natural Numbers
Informal description
The function `WithTop.some` from natural numbers to extended natural numbers is equal to the canonical embedding `Nat.cast`.
ENat.coe_inj theorem
{a b : ℕ} : (a : ℕ∞) = b ↔ a = b
Full source 
theorem coe_inj {a b : ℕ} : (a : ℕ∞) = b ↔ a = b := WithTop.coe_inj
Injectivity of the canonical embedding $\mathbb{N} \hookrightarrow \mathbb{N}_\infty$
Informal description
For any natural numbers $a$ and $b$, the canonical embeddings of $a$ and $b$ into the extended natural numbers $\mathbb{N}_\infty$ are equal if and only if $a = b$.
ENat.instSuccAddOrder instance
: SuccAddOrder ℕ∞
Full source 
instance : SuccAddOrder ℕ∞ where
  succ_eq_add_one x := by cases x <;> simp [SuccOrder.succ]
Successor Additive Order Structure on Extended Natural Numbers
Informal description
The extended natural numbers $\mathbb{N}_\infty$ form a successor additive order, where the successor operation is compatible with addition.
ENat.coe_zero theorem
: ((0 : ℕ) : ℕ∞) = 0
Full source 
theorem coe_zero : ((0 : ℕ) : ℕ∞) = 0 :=
  rfl
Embedding of Zero into Extended Natural Numbers: $(0 : \mathbb{N}_\infty) = 0$
Informal description
The canonical embedding of the natural number $0$ into the extended natural numbers $\mathbb{N}_\infty$ is equal to the zero element of $\mathbb{N}_\infty$, i.e., $(0 : \mathbb{N}_\infty) = 0$.
ENat.coe_one theorem
: ((1 : ℕ) : ℕ∞) = 1
Full source 
theorem coe_one : ((1 : ℕ) : ℕ∞) = 1 :=
  rfl
Embedding of One into Extended Natural Numbers: $(1 : \mathbb{N}_\infty) = 1$
Informal description
The canonical embedding of the natural number $1$ into the extended natural numbers $\mathbb{N}_\infty$ is equal to the multiplicative identity element $1$ in $\mathbb{N}_\infty$, i.e., $(1 : \mathbb{N}_\infty) = 1$.
ENat.coe_add theorem
(m n : ℕ) : ↑(m + n) = (m + n : ℕ∞)
Full source 
theorem coe_add (m n : ℕ) : ↑(m + n) = (m + n : ℕ∞) :=
  rfl
Embedding Preserves Addition in Extended Natural Numbers: $(m + n) = m + n$
Informal description
For any natural numbers $m$ and $n$, the canonical embedding of their sum into the extended natural numbers $\mathbb{N}_\infty$ is equal to the sum of their embeddings, i.e., $(m + n : \mathbb{N}_\infty) = (m : \mathbb{N}_\infty) + (n : \mathbb{N}_\infty)$.
ENat.coe_sub theorem
(m n : ℕ) : ↑(m - n) = (m - n : ℕ∞)
Full source 
@[simp, norm_cast]
theorem coe_sub (m n : ℕ) : ↑(m - n) = (m - n : ℕ∞) :=
  rfl
Embedding Preserves Subtraction in Extended Natural Numbers: $(m - n) = m - n$
Informal description
For any natural numbers $m$ and $n$, the canonical embedding of their difference into the extended natural numbers $\mathbb{N}_\infty$ is equal to the difference of their embeddings, i.e., $(m - n : \mathbb{N}_\infty) = (m : \mathbb{N}_\infty) - (n : \mathbb{N}_\infty)$.
ENat.coe_mul theorem
(m n : ℕ) : ↑(m * n) = (m * n : ℕ∞)
Full source 
@[simp] lemma coe_mul (m n : ℕ) : ↑(m * n) = (m * n : ℕ∞) := rfl
Embedding Preserves Multiplication in Extended Natural Numbers: $(m \cdot n) = m \cdot n$
Informal description
For any natural numbers $m$ and $n$, the canonical embedding of their product into the extended natural numbers $\mathbb{N}_\infty$ is equal to the product of their embeddings, i.e., $(m \cdot n : \mathbb{N}_\infty) = (m : \mathbb{N}_\infty) \cdot (n : \mathbb{N}_\infty)$.
ENat.mul_top theorem
(hm : m ≠ 0) : m * ⊤ = ⊤
Full source 
@[simp] theorem mul_top (hm : m ≠ 0) : m * ⊤ = ⊤ := WithTop.mul_top hm
Multiplication of Nonzero Extended Natural Number with Infinity Yields Infinity
Informal description
For any extended natural number $m \neq 0$, the product of $m$ and $\top$ (infinity) in $\mathbb{N}_\infty$ equals $\top$, i.e., $m \cdot \top = \top$.
ENat.top_mul theorem
(hm : m ≠ 0) : ⊤ * m = ⊤
Full source 
@[simp] theorem top_mul (hm : m ≠ 0) : ⊤ * m = ⊤ := WithTop.top_mul hm
Multiplication of Infinity by Nonzero Extended Natural Number
Informal description
For any extended natural number $m \neq 0$, the product of $\top$ (infinity) and $m$ in $\mathbb{N}_\infty$ equals $\top$.
ENat.mul_top' theorem
: m * ⊤ = if m = 0 then 0 else ⊤
Full source 
/-- A version of `mul_top` where the RHS is stated as an `ite` -/
theorem mul_top' : m * ⊤ = if m = 0 then 0 else ⊤ := WithTop.mul_top' m
Multiplication by Infinity in Extended Natural Numbers: $m \cdot \top = \text{if } m = 0 \text{ then } 0 \text{ else } \top$
Informal description
For any extended natural number $m$, the product $m \cdot \top$ equals $0$ if $m = 0$, and equals $\top$ otherwise.
ENat.top_mul' theorem
: ⊤ * m = if m = 0 then 0 else ⊤
Full source 
/-- A version of `top_mul` where the RHS is stated as an `ite` -/
theorem top_mul' : ⊤ * m = if m = 0 then 0 else ⊤ := WithTop.top_mul' m
Multiplication of Infinity by Extended Natural Number: $\top \cdot m = \text{ite}(m = 0, 0, \top)$
Informal description
For any extended natural number $m$, the product of $\top$ (infinity) and $m$ in $\mathbb{N}_\infty$ equals $0$ if $m = 0$, and equals $\top$ otherwise, i.e., $\top \cdot m = \begin{cases} 0 & \text{if } m = 0 \\ \top & \text{otherwise} \end{cases}$.
ENat.top_pow theorem
{n : ℕ} (hn : n ≠ 0) : (⊤ : ℕ∞) ^ n = ⊤
Full source 
@[simp] lemma top_pow {n : ℕ} (hn : n ≠ 0) : (⊤ : ℕ∞) ^ n = ⊤ := WithTop.top_pow hn
Power of Infinity in Extended Natural Numbers: $\infty^n = \infty$ for $n \neq 0$
Informal description
For any nonzero natural number $n$, the $n$-th power of $\infty$ in the extended natural numbers $\mathbb{N}_\infty$ is $\infty$, i.e., $\infty^n = \infty$.
ENat.pow_eq_top_iff theorem
{n : ℕ} : a ^ n = ⊤ ↔ a = ⊤ ∧ n ≠ 0
Full source 
@[simp] lemma pow_eq_top_iff {n : ℕ} : a ^ n = ⊤ ↔ a = ⊤ ∧ n ≠ 0 := WithTop.pow_eq_top_iff
Power Equals Infinity Condition in Extended Natural Numbers: $a^n = \infty \leftrightarrow (a = \infty \land n \neq 0)$
Informal description
For an extended natural number $a \in \mathbb{N}_\infty$ and a natural number $n \in \mathbb{N}$, the power $a^n$ equals $\infty$ if and only if $a = \infty$ and $n \neq 0$.
ENat.pow_ne_top_iff theorem
{n : ℕ} : a ^ n ≠ ⊤ ↔ a ≠ ⊤ ∨ n = 0
Full source 
lemma pow_ne_top_iff {n : ℕ} : a ^ n ≠ ⊤a ^ n ≠ ⊤ ↔ a ≠ ⊤ ∨ n = 0 := WithTop.pow_ne_top_iff
Non-infinity condition for powers in extended natural numbers: $a^n \neq \infty \leftrightarrow (a \neq \infty \lor n = 0)$
Informal description
For an extended natural number $a \in \mathbb{N}_\infty$ and a natural number $n \in \mathbb{N}$, the power $a^n$ is not equal to $\infty$ if and only if either $a \neq \infty$ or $n = 0$.
ENat.pow_lt_top_iff theorem
{n : ℕ} : a ^ n < ⊤ ↔ a < ⊤ ∨ n = 0
Full source 
@[simp] lemma pow_lt_top_iff {n : ℕ} : a ^ n < ⊤ ↔ a < ⊤ ∨ n = 0 := WithTop.pow_lt_top_iff
Strictly finite condition for powers in extended natural numbers: $a^n < \infty \leftrightarrow (a < \infty \lor n = 0)$
Informal description
For an extended natural number $a \in \mathbb{N}_\infty$ and a natural number $n \in \mathbb{N}$, the power $a^n$ is strictly less than $\infty$ if and only if either $a$ is strictly less than $\infty$ or $n = 0$.
ENat.lift definition
(x : ℕ∞) (h : x < ⊤) : ℕ
Full source 
/-- Convert a `ℕ∞` to a `ℕ` using a proof that it is not infinite. -/
def lift (x : ℕ∞) (h : x < ⊤) : ℕ := WithTop.untop x (WithTop.lt_top_iff_ne_top.mp h)
Conversion from finite extended natural number to natural number
Informal description
Given an extended natural number $x \in \mathbb{N}_\infty$ and a proof $h$ that $x$ is finite (i.e., $x < \infty$), the function returns the corresponding natural number obtained by removing the $\infty$ case.
ENat.coe_lift theorem
(x : ℕ∞) (h : x < ⊤) : (lift x h : ℕ∞) = x
Full source 
@[simp] theorem coe_lift (x : ℕ∞) (h : x < ⊤) : (lift x h : ℕ∞) = x :=
  WithTop.coe_untop x (WithTop.lt_top_iff_ne_top.mp h)
Embedding of Finite Extended Natural Number via Lift Equals Original
Informal description
For any extended natural number $x \in \mathbb{N}_\infty$ and a proof $h$ that $x$ is finite (i.e., $x < \infty$), the canonical embedding of the natural number obtained from `lift x h` back into $\mathbb{N}_\infty$ equals $x$.
ENat.lift_coe theorem
(n : ℕ) : lift (n : ℕ∞) (WithTop.coe_lt_top n) = n
Full source 
@[simp] theorem lift_coe (n : ℕ) : lift (n : ℕ∞) (WithTop.coe_lt_top n) = n := rfl
Lift of Cast Natural Number Equals Original
Informal description
For any natural number $n$, the lift of the extended natural number obtained by casting $n$ to $\mathbb{N}_\infty$ (which is finite) is equal to $n$ itself.
ENat.lift_lt_iff theorem
{x : ℕ∞} {h} {n : ℕ} : lift x h < n ↔ x < n
Full source 
@[simp] theorem lift_lt_iff {x : ℕ∞} {h} {n : ℕ} : liftlift x h < n ↔ x < n := WithTop.untop_lt_iff _
Inequality Preservation for Finite Extended Natural Numbers under Lift
Informal description
For any extended natural number $x \in \mathbb{N}_\infty$ with a proof $h$ that $x$ is finite (i.e., $x < \infty$), and for any natural number $n$, the inequality $\text{lift}(x, h) < n$ holds if and only if $x < n$ holds in $\mathbb{N}_\infty$.
ENat.lift_le_iff theorem
{x : ℕ∞} {h} {n : ℕ} : lift x h ≤ n ↔ x ≤ n
Full source 
@[simp] theorem lift_le_iff {x : ℕ∞} {h} {n : ℕ} : liftlift x h ≤ n ↔ x ≤ n := WithTop.untop_le_iff _
Inequality Preservation for Finite Extended Natural Numbers under Lift
Informal description
For any extended natural number $x \in \mathbb{N}_\infty$ with a proof $h$ that $x$ is finite (i.e., $x < \infty$), and for any natural number $n$, the inequality $\text{lift}(x, h) \leq n$ holds if and only if $x \leq n$ holds in $\mathbb{N}_\infty$.
ENat.lt_lift_iff theorem
{x : ℕ} {n : ℕ∞} {h} : x < lift n h ↔ x < n
Full source 
@[simp] theorem lt_lift_iff {x : ℕ} {n : ℕ∞} {h} : x < lift n h ↔ x < n := WithTop.lt_untop_iff _
Inequality Preservation in Lifting Finite Extended Natural Numbers to Natural Numbers
Informal description
For any natural number $x$ and extended natural number $n \in \mathbb{N}_\infty$ with a proof $h$ that $n$ is finite (i.e., $n < \infty$), the inequality $x < \text{lift}(n, h)$ holds if and only if $x < n$ holds in $\mathbb{N}_\infty$.
ENat.le_lift_iff theorem
{x : ℕ} {n : ℕ∞} {h} : x ≤ lift n h ↔ x ≤ n
Full source 
@[simp] theorem le_lift_iff {x : ℕ} {n : ℕ∞} {h} : x ≤ lift n h ↔ x ≤ n := WithTop.le_untop_iff _
Inequality Preservation in Lifting Finite Extended Natural Numbers to Natural Numbers
Informal description
For any natural number $x$ and extended natural number $n \in \mathbb{N}_\infty$ with a proof $h$ that $n$ is finite (i.e., $n < \infty$), the inequality $x \leq \text{lift}(n, h)$ holds if and only if $x \leq n$ holds in $\mathbb{N}_\infty$.
ENat.lift_zero theorem
: lift 0 (WithTop.coe_lt_top 0) = 0
Full source 
@[simp] theorem lift_zero : lift 0 (WithTop.coe_lt_top 0) = 0 := rfl
Lift of Zero in Extended Natural Numbers is Zero
Informal description
The lift of the extended natural number $0$ (which is finite) equals the natural number $0$, i.e., $\text{lift}(0) = 0$.
ENat.lift_one theorem
: lift 1 (WithTop.coe_lt_top 1) = 1
Full source 
@[simp] theorem lift_one : lift 1 (WithTop.coe_lt_top 1) = 1 := rfl
Lift of One in Extended Natural Numbers is One
Informal description
The lift of the extended natural number $1$ (which is finite) equals the natural number $1$, i.e., $\text{lift}(1) = 1$.
ENat.lift_ofNat theorem
(n : ℕ) [n.AtLeastTwo] : lift ofNat(n) (WithTop.coe_lt_top n) = OfNat.ofNat n
Full source 
@[simp] theorem lift_ofNat (n : ℕ) [n.AtLeastTwo] :
    lift ofNat(n) (WithTop.coe_lt_top n) = OfNat.ofNat n := rfl
Lift of Finite Extended Natural Number Corresponds to Original Natural Number
Informal description
For any natural number $n$ (with `n.AtLeastTwo`), the lift of the extended natural number `ofNat(n)` (which is finite) equals the natural number `n` itself, i.e., $\text{lift}(\text{ofNat}(n)) = n$.
ENat.add_lt_top theorem
{a b : ℕ∞} : a + b < ⊤ ↔ a < ⊤ ∧ b < ⊤
Full source 
@[simp] theorem add_lt_top {a b : ℕ∞} : a + b < ⊤ ↔ a < ⊤ ∧ b < ⊤ := WithTop.add_lt_top
Sum of Extended Natural Numbers is Finite if and only if Both Summands are Finite
Informal description
For any extended natural numbers $a$ and $b$ in $\mathbb{N}_\infty$, the sum $a + b$ is less than $\top$ (infinity) if and only if both $a$ and $b$ are less than $\top$.
ENat.lift_add theorem
(a b : ℕ∞) (h : a + b < ⊤) : lift (a + b) h = lift a (add_lt_top.1 h).1 + lift b (add_lt_top.1 h).2
Full source 
@[simp] theorem lift_add (a b : ℕ∞) (h : a + b < ⊤) :
    lift (a + b) h = lift a (add_lt_top.1 h).1 + lift b (add_lt_top.1 h).2 := by
  apply coe_inj.1
  simp
Additivity of Lift for Finite Extended Natural Numbers
Informal description
For any extended natural numbers $a$ and $b$ in $\mathbb{N}_\infty$ such that $a + b < \infty$, the lift of the sum $a + b$ equals the sum of the lifts of $a$ and $b$. That is, $\text{lift}(a + b) = \text{lift}(a) + \text{lift}(b)$, where $\text{lift}(a)$ and $\text{lift}(b)$ are the corresponding natural numbers obtained from $a$ and $b$ respectively.
ENat.canLift instance
: CanLift ℕ∞ ℕ (↑) (· ≠ ⊤)
Full source 
instance canLift : CanLift ℕ∞ ℕ (↑) (· ≠ ⊤) := WithTop.canLift
Lifting Condition for Extended Natural Numbers to Natural Numbers
Informal description
For the extended natural numbers $\mathbb{N}_\infty$, there exists a lifting operation from $\mathbb{N}_\infty$ to $\mathbb{N}$ that is defined for all elements except $\top$ (i.e., for all $x \in \mathbb{N}_\infty$ such that $x \neq \top$).
ENat.instWellFoundedRelation instance
: WellFoundedRelation ℕ∞
Full source 
instance : WellFoundedRelation ℕ∞ where
  rel := (· < ·)
  wf := IsWellFounded.wf
Well-founded Relation on Extended Natural Numbers
Informal description
The extended natural numbers $\mathbb{N}_\infty$ have a well-founded relation.
ENat.toNat definition
: ℕ∞ → ℕ
Full source 
/-- Conversion of `ℕ∞` to `ℕ` sending `∞` to `0`. -/
def toNat : ℕ∞ → ℕ := WithTop.untopD 0
Conversion from extended natural numbers to natural numbers (∞ ↦ 0)
Informal description
The function maps an extended natural number $n \in \mathbb{N}_\infty$ to a natural number, where $\infty$ is mapped to $0$ and any other element $k \in \mathbb{N}$ is mapped to $k$ itself.
ENat.toNatHom definition
: MonoidWithZeroHom ℕ∞ ℕ
Full source 
/-- Homomorphism from `ℕ∞` to `ℕ` sending `∞` to `0`. -/
def toNatHom : MonoidWithZeroHom ℕ∞ ℕ where
  toFun := toNat
  map_one' := rfl
  map_zero' := rfl
  map_mul' := WithTop.untopD_zero_mul
Monoid with zero homomorphism from extended natural numbers to natural numbers (∞ ↦ 0)
Informal description
The monoid with zero homomorphism from the extended natural numbers $\mathbb{N}_\infty$ to the natural numbers $\mathbb{N}$ that maps $\infty$ to $0$ and preserves the multiplicative identity and multiplication.
ENat.coe_toNatHom theorem
: toNatHom = toNat
Full source 
@[simp, norm_cast] lemma coe_toNatHom : toNatHom = toNat := rfl
Equality of `toNatHom` and `toNat` for Extended Natural Numbers
Informal description
The monoid with zero homomorphism `toNatHom` from extended natural numbers to natural numbers is equal to the conversion function `toNat`, i.e., $\text{toNatHom} = \text{toNat}$.
ENat.toNatHom_apply theorem
(n : ℕ) : toNatHom n = toNat n
Full source 
lemma toNatHom_apply (n : ℕ) : toNatHom n = toNat n := rfl
Equality of `toNatHom` and `toNat` on Natural Numbers
Informal description
For any natural number $n$, the monoid with zero homomorphism `toNatHom` applied to $n$ is equal to the conversion function `toNat` applied to $n$, i.e., $\text{toNatHom}(n) = \text{toNat}(n)$.
ENat.toNat_coe theorem
(n : ℕ) : toNat n = n
Full source 
@[simp]
theorem toNat_coe (n : ℕ) : toNat n = n :=
  rfl
Preservation of Natural Numbers under `toNat` Conversion
Informal description
For any natural number $n$, the conversion of $n$ to an extended natural number and back to a natural number via `toNat` yields $n$ itself, i.e., $\text{toNat}(n) = n$.
ENat.toNat_zero theorem
: toNat 0 = 0
Full source 
@[simp]
theorem toNat_zero : toNat 0 = 0 :=
  rfl
Conversion of Zero in Extended Natural Numbers to Natural Numbers
Informal description
The conversion of the extended natural number $0$ to a natural number via `toNat` yields $0$, i.e., $\text{toNat}(0) = 0$.
ENat.toNat_one theorem
: toNat 1 = 1
Full source 
@[simp]
theorem toNat_one : toNat 1 = 1 :=
  rfl
Conversion of One in Extended Natural Numbers to Natural Numbers
Informal description
The conversion of the extended natural number $1$ to a natural number via the `toNat` function yields $1$, i.e., $\text{toNat}(1) = 1$.
ENat.toNat_ofNat theorem
(n : ℕ) [n.AtLeastTwo] : toNat ofNat(n) = n
Full source 
@[simp]
theorem toNat_ofNat (n : ℕ) [n.AtLeastTwo] : toNat ofNat(n) = n :=
  rfl
Conversion of Extended Natural Number Representation Preserves Value for $n \geq 2$
Informal description
For any natural number $n$ (with $n \geq 2$), the conversion of the extended natural number $\text{ofNat}(n)$ via the `toNat` function yields $n$, i.e., $\text{toNat}(\text{ofNat}(n)) = n$.
ENat.toNat_top theorem
: toNat ⊤ = 0
Full source 
@[simp]
theorem toNat_top : toNat ⊤ = 0 :=
  rfl
Conversion of Infinity to Zero in Extended Natural Numbers
Informal description
The conversion of the extended natural number $\infty$ (denoted as $\top$) to a natural number via the `toNat` function yields $0$, i.e., $\text{toNat}(\infty) = 0$.
ENat.toNat_eq_zero theorem
: toNat n = 0 ↔ n = 0 ∨ n = ⊤
Full source 
@[simp] theorem toNat_eq_zero : toNattoNat n = 0 ↔ n = 0 ∨ n = ⊤ := WithTop.untopD_eq_self_iff
Zero Conversion Criterion for Extended Natural Numbers: $\text{toNat}(n) = 0 \leftrightarrow n = 0 \lor n = \infty$
Informal description
For any extended natural number $n \in \mathbb{N}_\infty$, the conversion to a natural number via `toNat` yields $0$ if and only if $n$ is either $0$ or $\infty$ (i.e., $n = 0$ or $n = \top$).
ENat.recTopCoe_zero theorem
{C : ℕ∞ → Sort*} (d : C ⊤) (f : ∀ a : ℕ, C a) : @recTopCoe C d f 0 = f 0
Full source 
@[simp]
theorem recTopCoe_zero {C : ℕ∞ → Sort*} (d : C ⊤) (f : ∀ a : ℕ, C a) : @recTopCoe C d f 0 = f 0 :=
  rfl
Recursor Evaluation at Zero for Extended Natural Numbers
Informal description
For any type family $C : \mathbb{N}_\infty \to \text{Sort}^*$, given a value $d \in C(\infty)$ and a function $f : \mathbb{N} \to C(a)$ for each $a \in \mathbb{N}$, the recursor $\text{recTopCoe}$ applied to $0$ evaluates to $f(0)$.
ENat.recTopCoe_one theorem
{C : ℕ∞ → Sort*} (d : C ⊤) (f : ∀ a : ℕ, C a) : @recTopCoe C d f 1 = f 1
Full source 
@[simp]
theorem recTopCoe_one {C : ℕ∞ → Sort*} (d : C ⊤) (f : ∀ a : ℕ, C a) : @recTopCoe C d f 1 = f 1 :=
  rfl
Recursor Evaluation at One for Extended Natural Numbers
Informal description
For any type family $C : \mathbb{N}_\infty \to \text{Sort}^*$, given a value $d \in C(\infty)$ and a function $f : \mathbb{N} \to C(a)$ for each $a \in \mathbb{N}$, the recursor $\text{recTopCoe}$ applied to $1$ evaluates to $f(1)$.
ENat.recTopCoe_ofNat theorem
{C : ℕ∞ → Sort*} (d : C ⊤) (f : ∀ a : ℕ, C a) (x : ℕ) [x.AtLeastTwo] : @recTopCoe C d f ofNat(x) = f (OfNat.ofNat x)
Full source 
@[simp]
theorem recTopCoe_ofNat {C : ℕ∞ → Sort*} (d : C ⊤) (f : ∀ a : ℕ, C a) (x : ℕ) [x.AtLeastTwo] :
    @recTopCoe C d f ofNat(x) = f (OfNat.ofNat x) :=
  rfl
Recursor Evaluation at Canonical Embedding of $x \geq 2$ in Extended Natural Numbers
Informal description
For any type family $C : \mathbb{N}_\infty \to \text{Sort}^*$, given a value $d \in C(\infty)$ and a function $f : \mathbb{N} \to C(a)$ for each $a \in \mathbb{N}$, the recursor $\text{recTopCoe}$ applied to the canonical embedding of a natural number $x \geq 2$ into $\mathbb{N}_\infty$ evaluates to $f(x)$.
ENat.top_ne_coe theorem
(a : ℕ) : ⊤ ≠ (a : ℕ∞)
Full source 
@[simp]
theorem top_ne_coe (a : ℕ) : ⊤⊤ ≠ (a : ℕ∞) :=
  nofun
$\infty \neq a$ in extended natural numbers
Informal description
For any natural number $a$, the element $\infty$ in the extended natural numbers $\mathbb{N}_\infty$ is not equal to the canonical embedding of $a$ into $\mathbb{N}_\infty$.
ENat.top_ne_ofNat theorem
(a : ℕ) [a.AtLeastTwo] : ⊤ ≠ (ofNat(a) : ℕ∞)
Full source 
@[simp]
theorem top_ne_ofNat (a : ℕ) [a.AtLeastTwo] : ⊤⊤ ≠ (ofNat(a) : ℕ∞) :=
  nofun
$\infty \neq a$ for $a \geq 2$ in extended natural numbers
Informal description
For any natural number $a \geq 2$, the element $\infty$ in the extended natural numbers $\mathbb{N}_\infty$ is not equal to the canonical embedding of $a$ into $\mathbb{N}_\infty$.
ENat.top_ne_zero theorem
: (⊤ : ℕ∞) ≠ 0
Full source 
@[simp] lemma top_ne_zero : (⊤ : ℕ∞) ≠ 0 := nofun
$\infty \neq 0$ in extended natural numbers
Informal description
The element $\infty$ in the extended natural numbers $\mathbb{N}_\infty$ is not equal to $0$.
ENat.top_ne_one theorem
: (⊤ : ℕ∞) ≠ 1
Full source 
@[simp] lemma top_ne_one : (⊤ : ℕ∞) ≠ 1 := nofun
$\infty \neq 1$ in extended natural numbers
Informal description
The element $\infty$ in the extended natural numbers $\mathbb{N}_\infty$ is not equal to $1$.
ENat.coe_ne_top theorem
(a : ℕ) : (a : ℕ∞) ≠ ⊤
Full source 
@[simp]
theorem coe_ne_top (a : ℕ) : (a : ℕ∞) ≠ ⊤ :=
  nofun
Natural numbers embedded in $\mathbb{N}_\infty$ are not infinity
Informal description
For any natural number $a$, the canonical embedding of $a$ into the extended natural numbers $\mathbb{N}_\infty$ is not equal to $\infty$.
ENat.ofNat_ne_top theorem
(a : ℕ) [a.AtLeastTwo] : (ofNat(a) : ℕ∞) ≠ ⊤
Full source 
@[simp]
theorem ofNat_ne_top (a : ℕ) [a.AtLeastTwo] : (ofNat(a) : ℕ∞) ≠ ⊤ :=
  nofun
Non-infinity of embedded natural numbers $\geq 2$ in $\mathbb{N}_\infty$
Informal description
For any natural number $a$ that is at least 2 (i.e., $a \geq 2$), the canonical embedding of $a$ into the extended natural numbers $\mathbb{N}_\infty$ is not equal to $\infty$.
ENat.zero_ne_top theorem
: 0 ≠ (⊤ : ℕ∞)
Full source 
@[simp] lemma zero_ne_top : 0 ≠ (⊤ : ℕ∞) := nofun
Non-equality of Zero and Infinity in Extended Natural Numbers
Informal description
In the extended natural numbers $\mathbb{N}_\infty$, the element $0$ is not equal to $\infty$.
ENat.one_ne_top theorem
: 1 ≠ (⊤ : ℕ∞)
Full source 
@[simp] lemma one_ne_top : 1 ≠ (⊤ : ℕ∞) := nofun
Inequality of One and Infinity in Extended Natural Numbers
Informal description
The extended natural number $1$ is not equal to $\infty$ in $\mathbb{N}_\infty$.
ENat.top_sub_coe theorem
(a : ℕ) : (⊤ : ℕ∞) - a = ⊤
Full source 
@[simp]
theorem top_sub_coe (a : ℕ) : (⊤ : ℕ∞) - a = ⊤ :=
  WithTop.top_sub_coe
Subtraction of Natural Number from Infinity in Extended Natural Numbers Yields Infinity
Informal description
For any natural number $a$, the subtraction of $a$ from infinity in the extended natural numbers $\mathbb{N}_\infty$ equals infinity, i.e., $\top - a = \top$.
ENat.top_sub_one theorem
: (⊤ : ℕ∞) - 1 = ⊤
Full source 
@[simp]
theorem top_sub_one : (⊤ : ℕ∞) - 1 = ⊤ :=
  top_sub_coe 1
Subtraction of One from Infinity in Extended Natural Numbers
Informal description
In the extended natural numbers $\mathbb{N}_\infty$, subtracting $1$ from $\infty$ yields $\infty$, i.e., $\infty - 1 = \infty$.
ENat.top_sub_ofNat theorem
(a : ℕ) [a.AtLeastTwo] : (⊤ : ℕ∞) - ofNat(a) = ⊤
Full source 
@[simp]
theorem top_sub_ofNat (a : ℕ) [a.AtLeastTwo] : (⊤ : ℕ∞) - ofNat(a) = ⊤ :=
  top_sub_coe a
Subtraction of At-Least-Two from Infinity in Extended Natural Numbers
Informal description
For any natural number $a \geq 2$, the subtraction of $a$ from infinity in the extended natural numbers $\mathbb{N}_\infty$ equals infinity, i.e., $\infty - a = \infty$.
ENat.top_pos theorem
: (0 : ℕ∞) < ⊤
Full source 
@[simp]
theorem top_pos : (0 : ℕ∞) < ⊤ :=
  WithTop.top_pos
Positivity of Infinity in Extended Natural Numbers
Informal description
In the extended natural numbers $\mathbb{N}_\infty$, the element $\infty$ is strictly greater than $0$, i.e., $0 < \infty$.
ENat.sub_top theorem
(a : ℕ∞) : a - ⊤ = 0
Full source 
theorem sub_top (a : ℕ∞) : a - ⊤ = 0 :=
  WithTop.sub_top
Subtraction of Infinity in Extended Natural Numbers Yields Zero
Informal description
For any extended natural number $a \in \mathbb{N}_\infty$, the subtraction of $\infty$ from $a$ equals $0$, i.e., $a - \infty = 0$.
ENat.coe_toNat_eq_self theorem
: ENat.toNat n = n ↔ n ≠ ⊤
Full source 
@[simp]
theorem coe_toNat_eq_self : ENat.toNatENat.toNat n = n ↔ n ≠ ⊤ :=
  ENat.recTopCoe (by decide) (fun _ => by simp [toNat_coe]) n
Equality of Extended Natural Number and its Natural Conversion iff Not Infinity
Informal description
For any extended natural number $n \in \mathbb{N}_\infty$, the canonical conversion of $n$ to a natural number equals $n$ itself if and only if $n$ is not equal to $\infty$.
ENat.toNat_eq_iff_eq_coe theorem
(n : ℕ∞) (m : ℕ) [NeZero m] : n.toNat = m ↔ n = m
Full source 
@[simp] lemma toNat_eq_iff_eq_coe (n : ℕ∞) (m : ℕ) [NeZero m] :
    n.toNat = m ↔ n = m := by
  cases n
  · simpa using NeZero.ne' m
  · simp
Equivalence of Natural Conversion and Equality for Nonzero Extended Natural Numbers
Informal description
For any extended natural number $n \in \mathbb{N}_\infty$ and any nonzero natural number $m$, the conversion of $n$ to a natural number equals $m$ if and only if $n$ is equal to $m$ (when viewed as an element of $\mathbb{N}_\infty$ via the canonical embedding).
ENat.coe_toNat_le_self theorem
(n : ℕ∞) : ↑(toNat n) ≤ n
Full source 
theorem coe_toNat_le_self (n : ℕ∞) : ↑(toNat n) ≤ n :=
  ENat.recTopCoe le_top (fun _ => le_rfl) n
Natural Conversion Bound: $\text{toNat}(n) \leq n$ in Extended Natural Numbers
Informal description
For any extended natural number $n \in \mathbb{N}_\infty$, the natural number obtained by applying the `toNat` function to $n$ (with $\infty$ mapped to $0$) is less than or equal to $n$ when viewed in $\mathbb{N}_\infty$.
ENat.toNat_add theorem
{m n : ℕ∞} (hm : m ≠ ⊤) (hn : n ≠ ⊤) : toNat (m + n) = toNat m + toNat n
Full source 
theorem toNat_add {m n : ℕ∞} (hm : m ≠ ⊤) (hn : n ≠ ⊤) : toNat (m + n) = toNat m + toNat n := by
  lift m to ℕ using hm
  lift n to ℕ using hn
  rfl
Additivity of Natural Conversion for Extended Natural Numbers
Informal description
For any extended natural numbers $m, n \in \mathbb{N}_\infty$ such that $m \neq \infty$ and $n \neq \infty$, the conversion of their sum to a natural number satisfies $\text{toNat}(m + n) = \text{toNat}(m) + \text{toNat}(n)$.
ENat.toNat_sub theorem
{n : ℕ∞} (hn : n ≠ ⊤) (m : ℕ∞) : toNat (m - n) = toNat m - toNat n
Full source 
theorem toNat_sub {n : ℕ∞} (hn : n ≠ ⊤) (m : ℕ∞) : toNat (m - n) = toNat m - toNat n := by
  lift n to ℕ using hn
  induction m
  · rw [top_sub_coe, toNat_top, zero_tsub]
  · rw [← coe_sub, toNat_coe, toNat_coe, toNat_coe]
Subtractivity of Natural Conversion for Extended Natural Numbers: $\text{toNat}(m - n) = \text{toNat}(m) - \text{toNat}(n)$
Informal description
For any extended natural number $n \in \mathbb{N}_\infty$ with $n \neq \infty$ and any extended natural number $m \in \mathbb{N}_\infty$, the conversion of their difference to a natural number satisfies $\text{toNat}(m - n) = \text{toNat}(m) - \text{toNat}(n)$.
ENat.toNat_mul theorem
(a b : ℕ∞) : (a * b).toNat = a.toNat * b.toNat
Full source 
theorem toNat_mul (a b : ℕ∞) : (a * b).toNat = a.toNat * b.toNat := by
  cases a <;> cases b <;> simp
  · rename_i b; cases b <;> simp
  · rename_i a; cases a <;> simp
  · rw [← coe_mul, toNat_coe]
Multiplicativity of Natural Conversion for Extended Natural Numbers: $\text{toNat}(a \cdot b) = \text{toNat}(a) \cdot \text{toNat}(b)$
Informal description
For any extended natural numbers $a, b \in \mathbb{N}_\infty$, the conversion of their product to a natural number equals the product of their individual conversions, i.e., $\text{toNat}(a \cdot b) = \text{toNat}(a) \cdot \text{toNat}(b)$.
ENat.toNat_eq_iff theorem
{m : ℕ∞} {n : ℕ} (hn : n ≠ 0) : toNat m = n ↔ m = n
Full source 
theorem toNat_eq_iff {m : ℕ∞} {n : ℕ} (hn : n ≠ 0) : toNattoNat m = n ↔ m = n := by
  induction m <;> simp [hn.symm]
Equivalence of Conversion and Equality for Extended Natural Numbers
Informal description
For any extended natural number $m \in \mathbb{N}_\infty$ and any nonzero natural number $n \in \mathbb{N}$, the conversion of $m$ to a natural number equals $n$ if and only if $m$ is equal to $n$. In other words, $\text{toNat}(m) = n \leftrightarrow m = n$.
ENat.toNat_le_of_le_coe theorem
{m : ℕ∞} {n : ℕ} (h : m ≤ n) : toNat m ≤ n
Full source 
lemma toNat_le_of_le_coe {m : ℕ∞} {n : ℕ} (h : m ≤ n) : toNat m ≤ n := by
  lift m to ℕ using ne_top_of_le_ne_top (coe_ne_top n) h
  simpa using h
Natural Conversion Preserves Order with Embedded Natural Numbers: $\text{toNat}(m) \leq n$ when $m \leq n$
Informal description
For any extended natural number $m \in \mathbb{N}_\infty$ and any natural number $n \in \mathbb{N}$, if $m \leq n$ (where $n$ is considered as an element of $\mathbb{N}_\infty$ via the canonical embedding), then the natural number obtained by applying the `toNat` function to $m$ is less than or equal to $n$.
ENat.toNat_le_toNat theorem
{m n : ℕ∞} (h : m ≤ n) (hn : n ≠ ⊤) : toNat m ≤ toNat n
Full source 
@[gcongr]
lemma toNat_le_toNat {m n : ℕ∞} (h : m ≤ n) (hn : n ≠ ⊤) : toNat m ≤ toNat n :=
  toNat_le_of_le_coe <| h.trans_eq (coe_toNat hn).symm
Order Preservation of Natural Conversion for Extended Natural Numbers: $\text{toNat}(m) \leq \text{toNat}(n)$ when $m \leq n$ and $n \neq \infty$
Informal description
For any extended natural numbers $m, n \in \mathbb{N}_\infty$ such that $m \leq n$ and $n \neq \infty$, the inequality $\text{toNat}(m) \leq \text{toNat}(n)$ holds.
ENat.succ_def theorem
(m : ℕ∞) : Order.succ m = m + 1
Full source 
@[simp]
theorem succ_def (m : ℕ∞) : Order.succ m = m + 1 :=
  Order.succ_eq_add_one m
Successor Definition for Extended Natural Numbers: $\text{succ}(m) = m + 1$
Informal description
For any extended natural number $m \in \mathbb{N}_\infty$, the successor of $m$ is equal to $m + 1$, i.e., $\text{succ}(m) = m + 1$.
ENat.lt_add_one_iff theorem
(hm : n ≠ ⊤) : m < n + 1 ↔ m ≤ n
Full source 
theorem lt_add_one_iff (hm : n ≠ ⊤) : m < n + 1 ↔ m ≤ n :=
  Order.lt_add_one_iff_of_not_isMax (not_isMax_iff_ne_top.mpr hm)
Characterization of Strict Inequality with Successor in Extended Natural Numbers: $m < n + 1 \leftrightarrow m \leq n$ when $n \neq \infty$
Informal description
For extended natural numbers $m, n \in \mathbb{N}_\infty$ with $n \neq \infty$, the inequality $m < n + 1$ holds if and only if $m \leq n$.
ENat.le_coe_iff theorem
{n : ℕ∞} {k : ℕ} : n ≤ ↑k ↔ ∃ (n₀ : ℕ), n = n₀ ∧ n₀ ≤ k
Full source 
theorem le_coe_iff {n : ℕ∞} {k : ℕ} : n ≤ ↑k ↔ ∃ (n₀ : ℕ), n = n₀ ∧ n₀ ≤ k :=
  WithTop.le_coe_iff
Characterization of Inequality Between Extended and Natural Numbers
Informal description
For an extended natural number $n \in \mathbb{N}_\infty$ and a natural number $k \in \mathbb{N}$, the inequality $n \leq k$ holds if and only if there exists a natural number $n_0 \in \mathbb{N}$ such that $n = n_0$ and $n_0 \leq k$.
ENat.not_lt_zero theorem
(n : ℕ∞) : ¬n < 0
Full source 
@[simp]
lemma not_lt_zero (n : ℕ∞) : ¬ n < 0 := by
  cases n <;> simp
No Extended Natural Number is Less Than Zero
Informal description
For any extended natural number $n \in \mathbb{N}_\infty$, it is not true that $n < 0$.
ENat.coe_lt_top theorem
(n : ℕ) : (n : ℕ∞) < ⊤
Full source 
@[simp]
lemma coe_lt_top (n : ℕ) : (n : ℕ∞) < ⊤ :=
  WithTop.coe_lt_top n
Natural Numbers are Strictly Below Infinity in Extended Naturals
Informal description
For any natural number $n \in \mathbb{N}$, the extended natural number obtained by casting $n$ into $\mathbb{N}_\infty$ is strictly less than $\top$ (the adjoined infinity element).
ENat.coe_lt_coe theorem
{n m : ℕ} : (n : ℕ∞) < (m : ℕ∞) ↔ n < m
Full source 
lemma coe_lt_coe {n m : ℕ} : (n : ℕ∞) < (m : ℕ∞) ↔ n < m := by simp
Preservation of Strict Order under Cast to Extended Natural Numbers
Informal description
For any natural numbers $n$ and $m$, the extended natural number obtained by casting $n$ into $\mathbb{N}_\infty$ is strictly less than the extended natural number obtained by casting $m$ into $\mathbb{N}_\infty$ if and only if $n < m$ in the usual ordering of natural numbers.
ENat.coe_le_coe theorem
{n m : ℕ} : (n : ℕ∞) ≤ (m : ℕ∞) ↔ n ≤ m
Full source 
lemma coe_le_coe {n m : ℕ} : (n : ℕ∞) ≤ (m : ℕ∞) ↔ n ≤ m := by simp
Preservation of Non-Strict Order under Cast to Extended Natural Numbers
Informal description
For any natural numbers $n$ and $m$, the extended natural number obtained by casting $n$ into $\mathbb{N}_\infty$ is less than or equal to the extended natural number obtained by casting $m$ into $\mathbb{N}_\infty$ if and only if $n \leq m$ in the usual ordering of natural numbers.
ENat.nat_induction theorem
{P : ℕ∞ → Prop} (a : ℕ∞) (h0 : P 0) (hsuc : ∀ n : ℕ, P n → P n.succ) (htop : (∀ n : ℕ, P n) → P ⊤) : P a
Full source 
@[elab_as_elim]
theorem nat_induction {P : ℕ∞ → Prop} (a : ℕ∞) (h0 : P 0) (hsuc : ∀ n : ℕ, P n → P n.succ)
    (htop : (∀ n : ℕ, P n) → P ⊤) : P a := by
  have A : ∀ n : ℕ, P n := fun n => Nat.recOn n h0 hsuc
  cases a
  · exact htop A
  · exact A _
Induction Principle for Extended Natural Numbers
Informal description
Let $P$ be a predicate on the extended natural numbers $\mathbb{N}_\infty$. Given an extended natural number $a \in \mathbb{N}_\infty$, if: 1. $P(0)$ holds, 2. For any natural number $n \in \mathbb{N}$, $P(n)$ implies $P(n+1)$, and 3. $P(\infty)$ holds whenever $P(n)$ holds for all $n \in \mathbb{N}$, then $P(a)$ holds for all $a \in \mathbb{N}_\infty$.
ENat.add_one_pos theorem
: 0 < n + 1
Full source 
lemma add_one_pos : 0 < n + 1 :=
  succ_def n ▸ Order.bot_lt_succ n
Positivity of Successor in Extended Natural Numbers: $0 < n + 1$
Informal description
For any extended natural number $n \in \mathbb{N}_\infty$, the sum $n + 1$ is strictly greater than $0$.
ENat.add_lt_add_iff_right theorem
{k : ℕ∞} (h : k ≠ ⊤) : n + k < m + k ↔ n < m
Full source 
lemma add_lt_add_iff_right {k : ℕ∞} (h : k ≠ ⊤) : n + k < m + k ↔ n < m :=
  WithTop.add_lt_add_iff_right h
Right Addition Preserves Strict Inequality in Extended Natural Numbers (Finite Case)
Informal description
For any extended natural numbers $n, m$ and any $k \in \mathbb{N}_\infty$ with $k \neq \infty$, the inequality $n + k < m + k$ holds if and only if $n < m$.
ENat.add_lt_add_iff_left theorem
{k : ℕ∞} (h : k ≠ ⊤) : k + n < k + m ↔ n < m
Full source 
lemma add_lt_add_iff_left {k : ℕ∞} (h : k ≠ ⊤) : k + n < k + m ↔ n < m :=
  WithTop.add_lt_add_iff_left h
Left Addition Preserves Strict Inequality in Extended Natural Numbers (Finite Case)
Informal description
For any extended natural numbers $n, m$ and any $k \in \mathbb{N}_\infty$ with $k \neq \infty$, the inequality $k + n < k + m$ holds if and only if $n < m$.
ENat.ne_top_iff_exists theorem
: n ≠ ⊤ ↔ ∃ m : ℕ, ↑m = n
Full source 
lemma ne_top_iff_exists : n ≠ ⊤n ≠ ⊤ ↔ ∃ m : ℕ, ↑m = n := WithTop.ne_top_iff_exists
Characterization of Finite Extended Natural Numbers via Natural Number Cast
Informal description
An extended natural number $n$ is not equal to $\infty$ if and only if there exists a natural number $m$ such that the canonical cast of $m$ into $\mathbb{N}_\infty$ equals $n$.
ENat.forall_natCast_le_iff_le theorem
: (∀ a : ℕ, a ≤ m → a ≤ n) ↔ m ≤ n
Full source 
/-- Version of `WithTop.forall_coe_le_iff_le` using `Nat.cast` rather than `WithTop.some`. -/
lemma forall_natCast_le_iff_le : (∀ a : ℕ, a ≤ m → a ≤ n) ↔ m ≤ n := WithTop.forall_coe_le_iff_le
Characterization of Order in Extended Natural Numbers via Natural Number Bounds
Informal description
For extended natural numbers $m, n \in \mathbb{N}_\infty$, the following are equivalent: 1. For every natural number $a \in \mathbb{N}$, if $a \leq m$ then $a \leq n$. 2. $m \leq n$.
ENat.exists_nat_gt theorem
(hn : n ≠ ⊤) : ∃ m : ℕ, n < m
Full source 
protected lemma exists_nat_gt (hn : n ≠ ⊤) : ∃ m : ℕ, n < m := by
  simp_rw [lt_iff_not_ge n]
  exact not_forall.mp <| eq_top_iff_forall_ge.2.mt hn
Existence of Natural Number Greater Than Finite Extended Natural Number
Informal description
For any extended natural number $n \in \mathbb{N}_\infty$ such that $n \neq \infty$, there exists a natural number $m \in \mathbb{N}$ satisfying $n < m$.
ENat.sub_eq_top_iff theorem
: a - b = ⊤ ↔ a = ⊤ ∧ b ≠ ⊤
Full source 
@[simp] lemma sub_eq_top_iff : a - b = ⊤ ↔ a = ⊤ ∧ b ≠ ⊤ := WithTop.sub_eq_top_iff
Difference Equals Infinity Condition for Extended Natural Numbers
Informal description
For extended natural numbers $a$ and $b$, the difference $a - b$ equals $\infty$ if and only if $a = \infty$ and $b \neq \infty$.
ENat.sub_ne_top_iff theorem
: a - b ≠ ⊤ ↔ a ≠ ⊤ ∨ b = ⊤
Full source 
lemma sub_ne_top_iff : a - b ≠ ⊤a - b ≠ ⊤ ↔ a ≠ ⊤ ∨ b = ⊤ := WithTop.sub_ne_top_iff
Difference of Extended Natural Numbers is Finite if and only if Either First Operand is Finite or Second Operand is Infinity
Informal description
For extended natural numbers $a$ and $b$, the difference $a - b$ is not equal to $\infty$ if and only if either $a \neq \infty$ or $b = \infty$.
ENat.addLECancellable_of_ne_top theorem
: a ≠ ⊤ → AddLECancellable a
Full source 
lemma addLECancellable_of_ne_top : a ≠ ⊤ → AddLECancellable a := WithTop.addLECancellable_of_ne_top
Left Cancellation of Addition for Finite Extended Natural Numbers
Informal description
For any extended natural number $a \in \mathbb{N}_\infty$ such that $a \neq \infty$, the addition operation is left cancellable with respect to the order relation. That is, for any $b, c \in \mathbb{N}_\infty$, if $a + b \leq a + c$, then $b \leq c$.
ENat.addLECancellable_of_lt_top theorem
: a < ⊤ → AddLECancellable a
Full source 
lemma addLECancellable_of_lt_top : a < ⊤ → AddLECancellable a := WithTop.addLECancellable_of_lt_top
Left Cancellation of Addition for Finite Extended Natural Numbers
Informal description
For any extended natural number $a \in \mathbb{N}_\infty$ such that $a < \infty$, the addition operation is left cancellable with respect to the order relation. That is, for any $b, c \in \mathbb{N}_\infty$, if $a + b \leq a + c$, then $b \leq c$.
ENat.addLECancellable_coe theorem
(a : ℕ) : AddLECancellable (a : ℕ∞)
Full source 
lemma addLECancellable_coe (a : ℕ) : AddLECancellable (a : ℕ∞) := WithTop.addLECancellable_coe _
Additive Left Cancellation Property for Cast Natural Numbers in $\mathbb{N}_\infty$
Informal description
For any natural number $a$, the extended natural number obtained by casting $a$ to $\mathbb{N}_\infty$ is additively left cancellable. That is, for any $b, c \in \mathbb{N}_\infty$, if $a + b \leq a + c$, then $b \leq c$.
ENat.le_sub_of_add_le_left theorem
(ha : a ≠ ⊤) : a + b ≤ c → b ≤ c - a
Full source 
protected lemma le_sub_of_add_le_left (ha : a ≠ ⊤) : a + b ≤ c → b ≤ c - a :=
  (addLECancellable_of_ne_top ha).le_tsub_of_add_le_left
Subtraction Lower Bound from Addition Inequality in Extended Natural Numbers
Informal description
For any extended natural numbers $a, b, c \in \mathbb{N}_\infty$ with $a \neq \infty$, if $a + b \leq c$, then $b \leq c - a$.
ENat.sub_sub_cancel theorem
(h : a ≠ ⊤) (h2 : b ≤ a) : a - (a - b) = b
Full source 
protected lemma sub_sub_cancel (h : a ≠ ⊤) (h2 : b ≤ a) : a - (a - b) = b :=
  (addLECancellable_of_ne_top <| ne_top_of_le_ne_top h tsub_le_self).tsub_tsub_cancel_of_le h2
Subtraction Cancellation Property for Finite Extended Natural Numbers
Informal description
For any extended natural numbers $a, b \in \mathbb{N}_\infty$ with $a \neq \infty$ and $b \leq a$, the subtraction operation satisfies $a - (a - b) = b$.
ENat.add_left_injective_of_ne_top theorem
{n : ℕ∞} (hn : n ≠ ⊤) : Function.Injective (· + n)
Full source 
lemma add_left_injective_of_ne_top {n : ℕ∞} (hn : n ≠ ⊤) : Function.Injective (· + n) := by
  intro a b e
  exact le_antisymm
    ((WithTop.add_le_add_iff_right hn).mp e.le)
    ((WithTop.add_le_add_iff_right hn).mp e.ge)
Left Addition by Finite Extended Natural Number is Injective
Informal description
For any extended natural number $n \neq \infty$, the function $x \mapsto x + n$ is injective on $\mathbb{N}_\infty$.
ENat.mul_left_strictMono theorem
(ha : a ≠ 0) (h_top : a ≠ ⊤) : StrictMono (a * ·)
Full source 
lemma mul_left_strictMono (ha : a ≠ 0) (h_top : a ≠ ⊤) : StrictMono (a * ·) := by
  lift a to ℕ using h_top
  intro x y hxy
  induction x with
  | top => simp at hxy
  | coe x =>
  induction y with
  | top =>
    simp only [mul_top ha, ← ENat.coe_mul]
    exact coe_lt_top (a * x)
  | coe y =>
  simp only
  rw [← ENat.coe_mul, ← ENat.coe_mul, ENat.coe_lt_coe]
  rw [ENat.coe_lt_coe] at hxy
  exact Nat.mul_lt_mul_of_pos_left hxy (Nat.pos_of_ne_zero (by simpa using ha))
Strict Monotonicity of Left Multiplication by Nonzero Finite Extended Natural Number
Informal description
For any extended natural number $a \neq 0$ and $a \neq \infty$, the function $x \mapsto a \cdot x$ is strictly monotone on $\mathbb{N}_\infty$. That is, for any $x, y \in \mathbb{N}_\infty$, if $x < y$ then $a \cdot x < a \cdot y$.
ENat.mul_right_strictMono theorem
(ha : a ≠ 0) (h_top : a ≠ ⊤) : StrictMono (· * a)
Full source 
lemma mul_right_strictMono (ha : a ≠ 0) (h_top : a ≠ ⊤) : StrictMono (· * a) := by
  simpa [show (· * a) = (a * ·) by simp [mul_comm]] using mul_left_strictMono ha h_top
Strict Monotonicity of Right Multiplication by Nonzero Finite Extended Natural Number
Informal description
For any extended natural number $a \neq 0$ and $a \neq \infty$, the function $x \mapsto x \cdot a$ is strictly monotone on $\mathbb{N}_\infty$. That is, for any $x, y \in \mathbb{N}_\infty$, if $x < y$ then $x \cdot a < y \cdot a$.
ENat.mul_le_mul_left_iff theorem
{x y : ℕ∞} (ha : a ≠ 0) (h_top : a ≠ ⊤) : a * x ≤ a * y ↔ x ≤ y
Full source 
@[simp]
lemma mul_le_mul_left_iff {x y : ℕ∞} (ha : a ≠ 0) (h_top : a ≠ ⊤) : a * x ≤ a * y ↔ x ≤ y :=
  (ENat.mul_left_strictMono ha h_top).le_iff_le
Left Multiplication Preserves Order in Extended Natural Numbers
Informal description
For any extended natural numbers $x, y \in \mathbb{N}_\infty$ and any nonzero finite extended natural number $a \in \mathbb{N}_\infty$ (i.e., $a \neq 0$ and $a \neq \infty$), the inequality $a \cdot x \leq a \cdot y$ holds if and only if $x \leq y$.
ENat.mul_le_mul_right_iff theorem
{x y : ℕ∞} (ha : a ≠ 0) (h_top : a ≠ ⊤) : x * a ≤ y * a ↔ x ≤ y
Full source 
@[simp]
lemma mul_le_mul_right_iff {x y : ℕ∞} (ha : a ≠ 0) (h_top : a ≠ ⊤) : x * a ≤ y * a ↔ x ≤ y :=
  (ENat.mul_right_strictMono ha h_top).le_iff_le
Right Multiplication Preserves Order in Extended Natural Numbers
Informal description
For any extended natural numbers $x, y \in \mathbb{N}_\infty$ and any nonzero finite extended natural number $a \in \mathbb{N}_\infty$ (i.e., $a \neq 0$ and $a \neq \infty$), the inequality $x \cdot a \leq y \cdot a$ holds if and only if $x \leq y$.
ENat.mul_le_mul_of_le_right theorem
{x y : ℕ∞} (hxy : x ≤ y) (ha : a ≠ 0) (h_top : a ≠ ⊤) : x * a ≤ y * a
Full source 
@[gcongr]
lemma mul_le_mul_of_le_right {x y : ℕ∞} (hxy : x ≤ y) (ha : a ≠ 0) (h_top : a ≠ ⊤) :
    x * a ≤ y * a := by
  simpa [ha, h_top]
Right Multiplication Preserves Order in Extended Natural Numbers
Informal description
For any extended natural numbers $x, y \in \mathbb{N}_\infty$ such that $x \leq y$, and for any nonzero extended natural number $a \in \mathbb{N}_\infty$ that is not $\infty$, we have $x \cdot a \leq y \cdot a$.
ENat.self_le_mul_right theorem
(a : ℕ∞) (hc : c ≠ 0) : a ≤ a * c
Full source 
lemma self_le_mul_right (a : ℕ∞) (hc : c ≠ 0) : a ≤ a * c := by
  obtain rfl | hne := eq_or_ne a ⊤
  · simp [top_mul hc]
  obtain rfl | h0 := eq_or_ne a 0
  · simp
  nth_rewrite 1 [← mul_one a, ENat.mul_le_mul_left_iff h0 hne, ENat.one_le_iff_ne_zero]
  assumption
Right Multiplication by Nonzero Element Increases Extended Natural Number
Informal description
For any extended natural number $a \in \mathbb{N}_\infty$ and any nonzero extended natural number $c \in \mathbb{N}_\infty$, we have $a \leq a \cdot c$.
ENat.self_le_mul_left theorem
(a : ℕ∞) (hc : c ≠ 0) : a ≤ c * a
Full source 
lemma self_le_mul_left (a : ℕ∞) (hc : c ≠ 0) : a ≤ c * a := by
  rw [mul_comm]
  exact ENat.self_le_mul_right a hc
Left Multiplication by Nonzero Element Increases Extended Natural Number
Informal description
For any extended natural number $a \in \mathbb{N}_\infty$ and any nonzero extended natural number $c \in \mathbb{N}_\infty$, we have $a \leq c \cdot a$.
ENat.add_one_natCast_le_withTop_of_lt theorem
{m : ℕ} {n : WithTop ℕ∞} (h : m < n) : (m + 1 : ℕ) ≤ n
Full source 
lemma add_one_natCast_le_withTop_of_lt {m : ℕ} {n : WithTop ℕ∞} (h : m < n) : (m + 1 : ℕ) ≤ n := by
  match n with
  | ⊤ => exact le_top
  | (⊤ : ℕ∞) => exact WithTop.coe_le_coe.2 (OrderTop.le_top _)
  | (n : ℕ) => simpa only [Nat.cast_le, ge_iff_le, Nat.cast_lt] using h
Successor Inequality in Extended Natural Numbers: $m < n \Rightarrow m + 1 \leq n$
Informal description
For any natural number $m$ and extended natural number $n$ (including $\infty$), if $m < n$, then the successor of $m$ (i.e., $m + 1$) is less than or equal to $n$.
ENat.coe_top_add_one theorem
: ((⊤ : ℕ∞) : WithTop ℕ∞) + 1 = (⊤ : ℕ∞)
Full source 
@[simp] lemma coe_top_add_one : ((⊤ : ℕ∞) : WithTop ℕ∞) + 1 = (⊤ : ℕ∞) := rfl
Absorption Property of Infinity in Extended Natural Numbers: $\top + 1 = \top$
Informal description
For the extended natural numbers $\mathbb{N}_\infty$, the sum of the top element $\top$ (representing infinity) and $1$ equals $\top$, i.e., $\top + 1 = \top$.
ENat.add_one_eq_coe_top_iff theorem
{n : WithTop ℕ∞} : n + 1 = (⊤ : ℕ∞) ↔ n = (⊤ : ℕ∞)
Full source 
@[simp] lemma add_one_eq_coe_top_iff {n : WithTop ℕ∞} : n + 1 = (⊤ : ℕ∞) ↔ n = (⊤ : ℕ∞) := by
  match n with
  | ⊤ => exact Iff.rfl
  | (⊤ : ℕ∞) => simp
  | (n : ℕ) =>
    norm_cast
    simp only [coe_ne_top, iff_false, ne_eq]
Characterization of Infinity in Extended Naturals: $n + 1 = \top \leftrightarrow n = \top$
Informal description
For any extended natural number $n \in \mathbb{N}_\infty$, the equation $n + 1 = \top$ holds if and only if $n = \top$, where $\top$ represents infinity in $\mathbb{N}_\infty$.
ENat.natCast_ne_coe_top theorem
(n : ℕ) : (n : WithTop ℕ∞) ≠ (⊤ : ℕ∞)
Full source 
@[simp] lemma natCast_ne_coe_top (n : ℕ) : (n : WithTop ℕ∞) ≠ (⊤ : ℕ∞) := nofun
Natural Numbers are Not Infinity in Extended Naturals: $n \neq \top$
Informal description
For any natural number $n$, the canonical embedding of $n$ into the extended natural numbers $\mathbb{N}_\infty$ is not equal to the top element $\top$ (representing infinity), i.e., $n \neq \top$.
ENat.one_le_iff_ne_zero_withTop theorem
{n : WithTop ℕ∞} : 1 ≤ n ↔ n ≠ 0
Full source 
lemma one_le_iff_ne_zero_withTop {n : WithTop ℕ∞} : 1 ≤ n ↔ n ≠ 0 :=
  ⟨fun h ↦ (zero_lt_one.trans_le h).ne',
    fun h ↦ add_one_natCast_le_withTop_of_lt (pos_iff_ne_zero.mpr h)⟩
Characterization of Nonzero Extended Naturals: $1 \leq n \leftrightarrow n \neq 0$
Informal description
For any extended natural number $n \in \mathbb{N}_\infty$, the inequality $1 \leq n$ holds if and only if $n \neq 0$.
ENat.natCast_le_of_coe_top_le_withTop theorem
{N : WithTop ℕ∞} (hN : (⊤ : ℕ∞) ≤ N) (n : ℕ) : n ≤ N
Full source 
lemma natCast_le_of_coe_top_le_withTop {N : WithTop ℕ∞} (hN : (⊤ : ℕ∞) ≤ N) (n : ℕ) : n ≤ N :=
  le_trans (mod_cast le_top) hN
Natural Numbers Bounded by Extended Naturals Containing Infinity
Informal description
For any extended natural number $N \in \mathbb{N}_\infty$ such that $\top \leq N$ (where $\top$ is the infinity element), and for any natural number $n \in \mathbb{N}$, we have $n \leq N$.
ENat.natCast_lt_of_coe_top_le_withTop theorem
{N : WithTop ℕ∞} (hN : (⊤ : ℕ∞) ≤ N) (n : ℕ) : n < N
Full source 
lemma natCast_lt_of_coe_top_le_withTop {N : WithTop ℕ∞} (hN : (⊤ : ℕ∞) ≤ N) (n : ℕ) : n < N :=
  lt_of_lt_of_le (mod_cast lt_add_one n) (natCast_le_of_coe_top_le_withTop hN (n + 1))
Natural Numbers are Strictly Less Than Extended Naturals Containing Infinity
Informal description
For any extended natural number $N \in \mathbb{N}_\infty$ such that $\infty \leq N$ and for any natural number $n \in \mathbb{N}$, we have $n < N$.
ENat.map definition
(f : ℕ → α) (k : ℕ∞) : WithTop α
Full source 
/--
Specialization of `WithTop.map` to `ENat`.
-/
def map (f : ℕ → α) (k : ℕ∞) : WithTop α := WithTop.map f k
Mapping a function over extended natural numbers
Informal description
The function `ENat.map` applies a function $f: \mathbb{N} \to \alpha$ to an extended natural number $k \in \mathbb{N}_\infty$, where $\mathbb{N}_\infty$ is the type of natural numbers extended with an infinity element. If $k$ is a natural number, the result is $f(k)$ lifted to `WithTop α`; if $k$ is infinity, the result is infinity in `WithTop α`.
ENat.map_top theorem
(f : ℕ → α) : map f ⊤ = ⊤
Full source 
@[simp]
theorem map_top (f : ℕ → α) : map f ⊤ = ⊤ := rfl
Mapping Infinity Preserves Infinity in Extended Natural Numbers
Informal description
For any function $f: \mathbb{N} \to \alpha$, the mapping of $f$ over the infinity element $\top$ in the extended natural numbers $\mathbb{N}_\infty$ yields the infinity element in $\text{WithTop } \alpha$, i.e., $\text{map } f \top = \top$.
ENat.map_coe theorem
(f : ℕ → α) (a : ℕ) : map f a = f a
Full source 
@[simp]
theorem map_coe (f : ℕ → α) (a : ℕ) : map f a = f a := rfl
Mapping Natural Numbers via Extended Natural Numbers Preserves Function Application
Informal description
For any function $f \colon \mathbb{N} \to \alpha$ and any natural number $a \in \mathbb{N}$, the mapping of $f$ over the extended natural number $a$ (viewed as an element of $\mathbb{N}_\infty$) equals $f(a)$, i.e., $\text{map}\,f\,a = f(a)$.
ENat.map_zero theorem
(f : ℕ → α) : map f 0 = f 0
Full source 
@[simp]
protected theorem map_zero (f : ℕ → α) : map f 0 = f 0 := rfl
Mapping Zero Preserves Function Application in Extended Natural Numbers
Informal description
For any function $f \colon \mathbb{N} \to \alpha$, the mapping of $f$ over the extended natural number $0$ equals $f(0)$, i.e., $\text{map}\,f\,0 = f(0)$.
ENat.map_one theorem
(f : ℕ → α) : map f 1 = f 1
Full source 
@[simp]
protected theorem map_one (f : ℕ → α) : map f 1 = f 1 := rfl
Mapping One Preserves Function Application in Extended Natural Numbers
Informal description
For any function $f \colon \mathbb{N} \to \alpha$, the mapping of $f$ over the extended natural number $1$ equals $f(1)$, i.e., $\text{map}\,f\,1 = f(1)$.
ENat.map_ofNat theorem
(f : ℕ → α) (n : ℕ) [n.AtLeastTwo] : map f ofNat(n) = f n
Full source 
@[simp]
theorem map_ofNat (f : ℕ → α) (n : ℕ) [n.AtLeastTwo] : map f ofNat(n) = f n := rfl
Mapping of Natural Numbers Preserves Function Application in Extended Naturals
Informal description
For any function $f \colon \mathbb{N} \to \alpha$ and any natural number $n \geq 2$, the mapping of $f$ over the extended natural number $n$ equals $f(n)$, i.e., $\text{map}\,f\,n = f(n)$.
ENat.map_eq_top_iff theorem
{f : ℕ → α} : map f n = ⊤ ↔ n = ⊤
Full source 
@[simp]
lemma map_eq_top_iff {f : ℕ → α} : mapmap f n = ⊤ ↔ n = ⊤ := WithTop.map_eq_top_iff
Mapping to Top in Extended Naturals is Equivalent to Input Being Top
Informal description
For any function $f: \mathbb{N} \to \alpha$ and any extended natural number $n \in \mathbb{N}_\infty$, the mapping $\text{map}\, f\, n$ equals the top element $\top$ if and only if $n$ itself is the top element $\top$ (i.e., $n = \infty$).
ENat.strictMono_map_iff theorem
{f : ℕ → α} [Preorder α] : StrictMono (ENat.map f) ↔ StrictMono f
Full source 
@[simp]
theorem strictMono_map_iff {f : ℕ → α} [Preorder α] : StrictMonoStrictMono (ENat.map f) ↔ StrictMono f :=
  WithTop.strictMono_map_iff
Strict Monotonicity Criterion for Extended Natural Number Mapping
Informal description
For any function $f: \mathbb{N} \to \alpha$ and any preorder $\alpha$, the extended function $\text{ENat.map}\, f : \mathbb{N}_\infty \to \alpha_\infty$ is strictly monotone if and only if $f$ is strictly monotone.
ENat.monotone_map_iff theorem
{f : ℕ → α} [Preorder α] : Monotone (ENat.map f) ↔ Monotone f
Full source 
@[simp]
theorem monotone_map_iff {f : ℕ → α} [Preorder α] : MonotoneMonotone (ENat.map f) ↔ Monotone f :=
  WithTop.monotone_map_iff
Monotonicity Criterion for Extended Natural Number Mapping
Informal description
For any function $f: \mathbb{N} \to \alpha$ and any preorder $\alpha$, the extended function $\text{ENat.map}\, f : \mathbb{N}_\infty \to \alpha_\infty$ is monotone if and only if $f$ is monotone.
ENat.map_natCast_nonneg theorem
: 0 ≤ n.map (Nat.cast : ℕ → α)
Full source 
@[simp] lemma map_natCast_nonneg : 0 ≤ n.map (Nat.cast : ℕ → α) := by cases n <;> simp
Nonnegativity of Extended Natural Number Casting
Informal description
For any extended natural number $n \in \mathbb{N}_\infty$, the image of $n$ under the mapping induced by the canonical embedding $\mathbb{N} \to \alpha$ is nonnegative, i.e., $0 \leq \text{map}(\text{Nat.cast})(n)$.
ENat.map_natCast_strictMono theorem
: StrictMono (map (Nat.cast : ℕ → α))
Full source 
lemma map_natCast_strictMono : StrictMono (map (Nat.cast : ℕ → α)) :=
  strictMono_map_iff.2 Nat.strictMono_cast
Strict Monotonicity of Extended Natural Number Casting
Informal description
The function mapping extended natural numbers to elements of type $\alpha$ via the canonical embedding $\mathbb{N} \to \alpha$ is strictly monotone. That is, for any extended natural numbers $m, n \in \mathbb{N}_\infty$, if $m < n$ then $\text{map}(\text{Nat.cast})(m) < \text{map}(\text{Nat.cast})(n)$ in $\alpha_\infty$.
ENat.map_natCast_injective theorem
: Injective (map (Nat.cast : ℕ → α))
Full source 
lemma map_natCast_injective : Injective (map (Nat.cast : ℕ → α)) := map_natCast_strictMono.injective
Injectivity of Extended Natural Number Casting via Canonical Embedding
Informal description
The mapping from extended natural numbers $\mathbb{N}_\infty$ to elements of type $\alpha$ via the canonical embedding $\mathbb{N} \to \alpha$ is injective. That is, for any extended natural numbers $m, n \in \mathbb{N}_\infty$, if $\text{map}(\text{Nat.cast})(m) = \text{map}(\text{Nat.cast})(n)$, then $m = n$.
ENat.map_natCast_inj theorem
: m.map (Nat.cast : ℕ → α) = n.map Nat.cast ↔ m = n
Full source 
@[simp] lemma map_natCast_inj : m.map (Nat.cast : ℕ → α) = n.map Nat.cast ↔ m = n :=
  map_natCast_injective.eq_iff
Injectivity of Canonical Embedding for Extended Natural Numbers
Informal description
For any extended natural numbers $m, n \in \mathbb{N}_\infty$, the canonical embedding of $m$ into $\alpha$ equals the canonical embedding of $n$ into $\alpha$ if and only if $m = n$. In other words, the mapping $\text{map}(\text{Nat.cast}) : \mathbb{N}_\infty \to \alpha_\infty$ is injective.
ENat.map_natCast_eq_zero theorem
: n.map (Nat.cast : ℕ → α) = 0 ↔ n = 0
Full source 
@[simp] lemma map_natCast_eq_zero : n.map (Nat.cast : ℕ → α) = 0 ↔ n = 0 := by
  simp [← map_natCast_inj (α := α)]
Canonical Embedding of Extended Natural Numbers is Zero if and only if $n = 0$
Informal description
For any extended natural number $n \in \mathbb{N}_\infty$, the canonical embedding of $n$ into $\alpha$ via the natural number casting function is equal to $0$ if and only if $n = 0$.
ENat.map_add theorem
{β F} [Add β] [FunLike F ℕ β] [AddHomClass F ℕ β] (f : F) (a b : ℕ∞) : (a + b).map f = a.map f + b.map f
Full source 
@[simp]
protected theorem map_add {β F} [Add β] [FunLike F ℕ β] [AddHomClass F ℕ β]
    (f : F) (a b : ℕ∞) : (a + b).map f = a.map f + b.map f :=
  WithTop.map_add f a b
Additivity of Mapping over Extended Natural Numbers
Informal description
Let $\beta$ be a type with an addition operation, and let $F$ be a function-like type from natural numbers to $\beta$ that preserves addition. For any extended natural numbers $a, b \in \mathbb{N}_\infty$ and any function $f \in F$, the mapping of the sum $a + b$ under $f$ equals the sum of the mappings of $a$ and $b$ under $f$, i.e., $$(a + b).map\, f = a.map\, f + b.map\, f.$$
OneHom.ENatMap definition
{N : Type*} [One N] (f : OneHom ℕ N) : OneHom ℕ∞ (WithTop N)
Full source 
/-- A version of `ENat.map` for `OneHom`s. -/
-- @[to_additive (attr := simps -fullyApplied)
--   "A version of `ENat.map` for `ZeroHom`s"]
protected def _root_.OneHom.ENatMap {N : Type*} [One N] (f : OneHom ℕ N) :
    OneHom ℕ∞ (WithTop N) where
  toFun := ENat.map f
  map_one' := by simp
Extension of multiplicative identity-preserving homomorphism to extended natural numbers
Informal description
Given a type `N` with a multiplicative identity and a multiplicative homomorphism `f : ℕ → N` that preserves the identity, the function `OneHom.ENatMap` extends `f` to a multiplicative homomorphism from the extended natural numbers `ℕ∞` (which includes infinity) to `WithTop N`. The extension maps infinity to infinity and applies `f` to finite natural numbers, preserving the multiplicative identity.
ZeroHom.ENatMap definition
{N : Type*} [Zero N] (f : ZeroHom ℕ N) : ZeroHom ℕ∞ (WithTop N)
Full source 
/-- A version of `ENat.map` for `ZeroHom`s. -/
protected def _root_.ZeroHom.ENatMap {N : Type*} [Zero N] (f : ZeroHom ℕ N) :
    ZeroHom ℕ∞ (WithTop N) where
  toFun := ENat.map f
  map_zero' := by simp
Extension of zero-preserving homomorphism to extended natural numbers
Informal description
Given a type `N` with a zero element and a zero-preserving homomorphism `f` from the natural numbers to `N`, the function `ZeroHom.ENatMap` extends `f` to a zero-preserving homomorphism from the extended natural numbers `ℕ∞` (which includes infinity) to `WithTop N`. The extension maps infinity to infinity and applies `f` to finite natural numbers.
AddHom.ENatMap definition
{N : Type*} [Add N] (f : AddHom ℕ N) : AddHom ℕ∞ (WithTop N)
Full source 
/-- A version of `WithTop.map` for `AddHom`s. -/
@[simps -fullyApplied]
protected def _root_.AddHom.ENatMap {N : Type*} [Add N] (f : AddHom ℕ N) :
    AddHom ℕ∞ (WithTop N) where
  toFun := ENat.map f
  map_add' := ENat.map_add f
Extension of additive homomorphism to extended natural numbers
Informal description
Given a type `N` with an addition operation and an additive homomorphism `f : ℕ → N`, the function `AddHom.ENatMap` extends `f` to an additive homomorphism from the extended natural numbers `ℕ∞` (which includes infinity) to `WithTop N`. The extension maps infinity to infinity and applies `f` to finite natural numbers, preserving the addition operation.
AddMonoidHom.ENatMap definition
{N : Type*} [AddZeroClass N] (f : ℕ →+ N) : ℕ∞ →+ WithTop N
Full source 
/-- A version of `WithTop.map` for `AddMonoidHom`s. -/
@[simps -fullyApplied]
protected def _root_.AddMonoidHom.ENatMap {N : Type*} [AddZeroClass N]
    (f : ℕℕ →+ N) : ℕ∞ℕ∞ →+ WithTop N :=
  { ZeroHom.ENatMap f.toZeroHom, AddHom.ENatMap f.toAddHom with toFun := ENat.map f }
Extension of additive monoid homomorphism to extended natural numbers
Informal description
Given an additive monoid homomorphism $f \colon \mathbb{N} \to N$ where $N$ is an additive monoid with zero, the function $\text{AddMonoidHom.ENatMap}$ extends $f$ to an additive monoid homomorphism from the extended natural numbers $\mathbb{N}_\infty$ (which includes infinity) to $\text{WithTop}\, N$. The extension maps infinity to infinity, preserves the additive identity and addition operation, and applies $f$ to finite natural numbers.
MonoidWithZeroHom.ENatMap definition
{S : Type*} [MulZeroOneClass S] [DecidableEq S] [Nontrivial S] (f : ℕ →*₀ S) (hf : Function.Injective f) : ℕ∞ →*₀ WithTop S
Full source 
/-- A version of `ENat.map` for `MonoidWithZeroHom`s. -/
@[simps -fullyApplied]
protected def _root_.MonoidWithZeroHom.ENatMap {S : Type*} [MulZeroOneClass S] [DecidableEq S]
    [Nontrivial S] (f : ℕℕ →*₀ S)
    (hf : Function.Injective f) : ℕ∞ℕ∞ →*₀ WithTop S :=
  { f.toZeroHom.ENatMap, f.toMonoidHom.toOneHom.ENatMap with
    toFun := ENat.map f
    map_mul' := fun x y => by
      have : ∀ z, mapmap f z = 0 ↔ z = 0 := fun z =>
        (Option.map_injective hf).eq_iff' f.toZeroHom.ENatMap.map_zero
      rcases Decidable.eq_or_ne x 0 with (rfl | hx)
      · simp
      rcases Decidable.eq_or_ne y 0 with (rfl | hy)
      · simp
      induction' x with x
      · simp [hy, this]
      induction' y with y
      · have : (f x : WithTop S) ≠ 0 := by simpa [hf.eq_iff' (map_zero f)] using hx
        simp [mul_top hx, WithTop.mul_top this]
      · simp [← Nat.cast_mul, ← coe_mul] }
Extension of monoid-with-zero homomorphism to extended natural numbers
Informal description
Given a type `S` with a multiplicative monoid structure that includes a zero element and a multiplicative identity, and given a monoid-with-zero homomorphism `f : ℕ →*₀ S` that is injective, the function `MonoidWithZeroHom.ENatMap` extends `f` to a monoid-with-zero homomorphism from the extended natural numbers `ℕ∞` (which includes infinity) to `WithTop S`. The extension maps infinity to infinity, preserves the multiplicative identity and zero, and applies `f` to finite natural numbers while respecting multiplication.
RingHom.ENatMap definition
{S : Type*} [CommSemiring S] [PartialOrder S] [CanonicallyOrderedAdd S] [DecidableEq S] [Nontrivial S] (f : ℕ →+* S) (hf : Function.Injective f) : ℕ∞ →+* WithTop S
Full source 
/-- A version of `ENat.map` for `RingHom`s. -/
@[simps -fullyApplied]
protected def _root_.RingHom.ENatMap {S : Type*} [CommSemiring S] [PartialOrder S]
    [CanonicallyOrderedAdd S]
    [DecidableEq S] [Nontrivial S] (f : ℕℕ →+* S) (hf : Function.Injective f) : ℕ∞ℕ∞ →+* WithTop S :=
  {MonoidWithZeroHom.ENatMap f.toMonoidWithZeroHom hf, f.toAddMonoidHom.ENatMap with}
Extension of ring homomorphism to extended natural numbers
Informal description
Given a commutative semiring $S$ with a partial order that is canonically ordered additively, and given an injective ring homomorphism $f \colon \mathbb{N} \to S$, the function $\text{RingHom.ENatMap}$ extends $f$ to a ring homomorphism from the extended natural numbers $\mathbb{N}_\infty$ (which includes infinity) to $\text{WithTop}\, S$. The extension maps infinity to infinity, preserves the additive and multiplicative structures, and applies $f$ to finite natural numbers while respecting both addition and multiplication.
WithBot.lt_add_one_iff theorem
{n : WithBot ℕ∞} {m : ℕ} : n < m + 1 ↔ n ≤ m
Full source 
lemma WithBot.lt_add_one_iff {n : WithBot ℕ∞} {m : ℕ} : n < m + 1 ↔ n ≤ m := by
  rw [← WithBot.coe_one, ← ENat.coe_one, WithBot.coe_natCast, ← Nat.cast_add, ← WithBot.coe_natCast]
  cases n
  · simp only [bot_le, iff_true, WithBot.bot_lt_coe]
  · rw [WithBot.coe_lt_coe, Nat.cast_add, ENat.coe_one, ENat.lt_add_one_iff (ENat.coe_ne_top _),
      ← WithBot.coe_le_coe, WithBot.coe_natCast]
Characterization of Strict Inequality with Successor in Extended Natural Numbers: $n < m + 1 \leftrightarrow n \leq m$
Informal description
For any extended natural number $n \in \mathbb{N}_\infty$ (possibly including $\infty$) and any natural number $m \in \mathbb{N}$, the inequality $n < m + 1$ holds if and only if $n \leq m$.
WithBot.add_one_le_iff theorem
{n : ℕ} {m : WithBot ℕ∞} : n + 1 ≤ m ↔ n < m
Full source 
lemma WithBot.add_one_le_iff {n : ℕ} {m : WithBot ℕ∞} : n + 1 ≤ m ↔ n < m := by
  rw [← WithBot.coe_one, ← ENat.coe_one, WithBot.coe_natCast, ← Nat.cast_add, ← WithBot.coe_natCast]
  cases m
  · simp
  · rw [WithBot.coe_le_coe, ENat.coe_add, ENat.coe_one, ENat.add_one_le_iff (ENat.coe_ne_top n),
      ← WithBot.coe_lt_coe, WithBot.coe_natCast]
Inequality Characterization for Extended Natural Numbers: $n + 1 \leq m \leftrightarrow n < m$
Informal description
For any natural number $n$ and any extended natural number $m$ (possibly including infinity), the inequality $n + 1 \leq m$ holds if and only if $n < m$.