ENat.top_sub_coe
theorem ENat.top_sub_coe : ∀ (a : ℕ), ⊤ - ↑a = ⊤
This theorem states that for any natural number `a`, the difference between the top element of the extended natural numbers (notated as `⊤`) and the natural number `a` is just `⊤`. In other words, subtracting any natural number from infinity still results in infinity.
More concisely: For any natural number `a`, `⊤ - a = ⊤` in the extended natural numbers.
|
ENat.coe_toNat
theorem ENat.coe_toNat : ∀ {n : ℕ∞}, n ≠ ⊤ → ↑(ENat.toNat n) = n
This theorem, referred to as an alias of the reverse direction of `ENat.coe_toNat_eq_self`, asserts that for any extended natural number `n` (represented as `ℕ∞`, where `∞` signifies infinity), provided that `n` is not equal to `∞`, the natural number obtained by converting `n` using the function `ENat.toNat` and then coercing back to an extended natural number yields the original extended natural number `n`. In other words, if `n` is a finite extended natural number, its conversion to a regular natural number and back to an extended natural number is a lossless operation.
More concisely: For all finite extended natural numbers `n`, `ENat.toNat (ENat.coeToNat n) = n`.
|
Mathlib.Data.ENat.Basic._auxLemma.5
theorem Mathlib.Data.ENat.Basic._auxLemma.5 : ∀ (a : ℕ), (↑a = ⊤) = False
This theorem states that for any natural number `a`, the proposition that the coerced value of `a` is equal to infinity (`⊤`) is always false. In other words, no natural number can equal infinity when typecast to an extended natural number (ENat) in Lean 4.
More concisely: For all natural numbers `a`, the coerced value `a` to ENat is not equal to infinity (⊤).
|
ENat.toNat_coe
theorem ENat.toNat_coe : ∀ (n : ℕ), ENat.toNat ↑n = n
This theorem states that for any natural number `n`, the function `ENat.toNat`, which converts extended natural numbers (including infinity) to natural numbers by mapping infinity to zero, when applied to the coercion of `n` to an extended natural number, will yield `n` itself. In mathematical terms, for any natural number `n`, we have `ENat.toNat ↑n = n`, which means the function `ENat.toNat` is an identity function for natural numbers in the context of the extended natural numbers system.
More concisely: For any natural number `n`, `ENat.toNat (coe toENat n) = n`. (Here, `coe` is the coercion function from natural numbers to extended natural numbers, and `toENat` is the conversion function from natural numbers to extended natural numbers.)
|
ENat.one_le_iff_ne_zero
theorem ENat.one_le_iff_ne_zero : ∀ {n : ℕ∞}, 1 ≤ n ↔ n ≠ 0
This theorem states that for any natural number `n` that can take on the value of infinity (`ℕ∞`), the condition `1 ≤ n` is logically equivalent to `n ≠ 0`. In other words, in the extended natural numbers, `n` being greater than or equal to one implies that it is not equal to zero, and vice versa.
More concisely: For natural numbers `n` including infinity (`ℕ∞`), `1 ≤ n` is logically equivalent to `n ≠ 0`.
|
ENat.coe_toNat_eq_self
theorem ENat.coe_toNat_eq_self : ∀ {n : ℕ∞}, ↑(ENat.toNat n) = n ↔ n ≠ ⊤
The theorem `ENat.coe_toNat_eq_self` states that for any natural number `n` extended to include infinity (`ℕ∞`), the natural number obtained by applying the function `ENat.toNat` to `n` and then coercing it to `ℕ∞` again, is equal to `n` if and only if `n` is not equal to infinity (`⊤`). Essentially, this is saying that the `ENat.toNat` function correctly converts any finite extended natural number to a natural number and back, but it sends infinity to zero.
More concisely: For any extended natural number `n`, `ENat.toNat n = n` if and only if `n` is finite.
|
ENat.some_eq_coe
theorem ENat.some_eq_coe : WithTop.some = Nat.cast
This theorem establishes an equivalence between the `WithTop.some` function and the `Nat.cast` function in the context of Extended Natural numbers (`ENat`). The `WithTop` lemmas generally work with `WithTop.some`, but the conventional form to perform the coercion from a Natural number (`ℕ`) to its extended version (`ℕ∞`) is `Nat.cast`. Thus, this theorem essentially shows that these two operations of embedding a natural number into the extended natural numbers are the same.
More concisely: The theorem asserts that the `WithTop.some` function and the `Nat.cast` function are equal for extending natural numbers.
|
ENat.succ_def
theorem ENat.succ_def : ∀ (m : ℕ∞), Order.succ m = m + 1
This theorem states that for any extended natural number `m` (expressed as `m : ℕ∞`), the successor of `m` under the defined order (`Order.succ m`) is equivalent to the sum of `m` and 1 (`m + 1`). In other words, the successor of any extended natural number is simply that number increased by one.
More concisely: For any extended natural number `m`, `Order.succ m` is equivalent to `m + 1`.
|