PartENat.withTopEquiv_natCast
theorem PartENat.withTopEquiv_natCast : ∀ (n : ℕ), PartENat.withTopEquiv ↑n = ↑n
The theorem `PartENat.withTopEquiv_natCast` states that for all natural numbers `n`, the equivalence between `PartENat` and the extended natural numbers `ℕ∞` (which is defined by the function `PartENat.withTopEquiv`), when applied to the embedding of `n` into `PartENat` (denoted by `↑n`), results in the embedding of `n` into `ℕ∞` (also denoted by `↑n`). In other words, this theorem asserts that the equivalence preserves the embedding of natural numbers into these two types.
More concisely: The theorem `PartENat.withTopEquiv_natCast` asserts that the natural number embedding function `↑` is preserved under the equivalence `PartENat.withTopEquiv` between `PartENat` and `ℕ∞`.
|
PartENat.coe_lt_coe
theorem PartENat.coe_lt_coe : ∀ {x y : ℕ}, ↑x < ↑y ↔ x < y
This theorem states that for all natural numbers `x` and `y`, the operation of casting `x` and `y` into the `PartENat` type and comparing them is equivalent to directly comparing `x` and `y` in their original type. In other words, the inequality holds in the `PartENat` type if and only if it holds in the `Nat` type. Here, the `PartENat` type refers to partial extended natural numbers, which includes all natural numbers plus infinity.
More concisely: For all natural numbers x and y, x < y in Nat if and only if x.toPartENat() < y.toPartENat() in PartENat.
|
PartENat.toWithTop_top'
theorem PartENat.toWithTop_top' : ∀ {h : Decidable ⊤.Dom}, ⊤.toWithTop = ⊤
This theorem states that for any decidable instance `h` of the domain of the top element `⊤`, the operation of converting this top element from a partial natural number (`PartENat`) to a natural number with infinity (`ℕ∞`) using the `toWithTop` function will yield the top element. In other words, converting the top element of `PartENat` to `ℕ∞` preserves the topness of the element.
More concisely: For any decidable instance `h` of the domain, `toWithTop h ⊤ = ⊤` in `ℕ∞`, where `⊤` is the top element in `PartENat`.
|
PartENat.add_one_le_of_lt
theorem PartENat.add_one_le_of_lt : ∀ {x y : PartENat}, x < y → x + 1 ≤ y
This theorem states that for any two elements `x` and `y` of the type `PartENat`, which consists of natural numbers along with an infinite element (`⊤`), if `x` is strictly less than `y`, then `x + 1` is less than or equal to `y`. This corresponds to the intuitive idea that adding one to a number does not exceed the next number, unless the next number is infinity.
More concisely: For all `x` and `y` in `PartENat`, if `x < y`, then `x + 1 ≤ y`.
|
PartENat.get_eq_iff_eq_coe
theorem PartENat.get_eq_iff_eq_coe : ∀ {a : PartENat} {ha : a.Dom} {b : ℕ}, a.get ha = b ↔ a = ↑b
This theorem states that for any partial natural number `a` with a defined domain `ha` and another natural number `b`, the value of `a` when applied to `ha` equals `b` if and only if `a` is the co-domain of `b`. In other words, a partial natural number is equivalent to a co-domain natural number if and only if their associated values are the same.
More concisely: For any partial natural number `a` with domain `ha` and natural number `b`, `ha a = b` if and only if `a = Σ i, i := 0 ^ ha.size, b i`. (In other words, `a` is the co-domain of `b`).
|
PartENat.ne_top_of_lt
theorem PartENat.ne_top_of_lt : ∀ {x y : PartENat}, x < y → x ≠ ⊤
This theorem states that for any two elements `x` and `y` of the type `PartENat`, which represents the natural numbers extended with a symbol for infinity (`⊤`), if `x` is less than `y` (`x < y`), then `x` cannot be infinity (`x ≠ ⊤`). In other words, no natural number or infinity (represented by `x`) that is less than another number or infinity (represented by `y`) can be infinity itself.
More concisely: If `x` is a natural number or infinity (PartENat) and `x` is less than `y` (PartENat), then `x` is not equal to infinity (`x ≠ ⊤`).
|
PartENat.some_eq_natCast
theorem PartENat.some_eq_natCast : ∀ (n : ℕ), ↑n = ↑n
This theorem states that for every natural number 'n', the result of casting 'n' to some other type (denoted by the ↑ symbol) is equal to the result of casting 'n' to the same other type. Essentially, it's saying that the process of type-casting a natural number is consistent and will always yield the same result when applied to the same input.
More concisely: For every natural number n, ↑n = ↑n, where ↑ denotes type-casting to some other type.
|
PartENat.lt_coe_iff
theorem PartENat.lt_coe_iff : ∀ (x : PartENat) (n : ℕ), x < ↑n ↔ ∃ (h : x.Dom), x.get h < n
This theorem states that for any partially defined natural number `x` and any natural number `n`, `x` is less than `n` if and only if there exists a proof `h` that `x` is defined (i.e., `x.Dom` is true) and the value of `x` obtained using this proof (i.e., `x.get h`) is less than `n`. In other words, a partially defined natural number is less than a given natural number if and only if it is defined and its value is less than that given number.
More concisely: For any partially defined natural number `x` and natural number `n`, `x` is less than `n` if and only if `x` is defined and `x < n`.
|
PartENat.coe_le_coe
theorem PartENat.coe_le_coe : ∀ {x y : ℕ}, ↑x ≤ ↑y ↔ x ≤ y
This theorem states that for any two natural numbers `x` and `y`, the statement "the partial extended natural number corresponding to `x` is less than or equal to the partial extended natural number corresponding to `y`" is equivalent to "x is less than or equal to y". In other words, the partial extended natural number representation of a number preserves the order of natural numbers.
More concisely: The theorem asserts that for all natural numbers x and y, x ≤ y if and only if the partial extended natural number representing x is less than or equal to the partial extended natural number representing y.
|
PartENat.top_add
theorem PartENat.top_add : ∀ (x : PartENat), ⊤ + x = ⊤
This theorem states that for every element `x` of the type `PartENat`, which represents the set of natural numbers extended with infinity (`⊤`), the sum of `⊤` and `x` always equals `⊤`. In other words, it captures the mathematical concept that infinity added to any extended natural number (including infinity itself) is still infinity.
More concisely: For every `x` in `PartENat`, `⊤ + x = ⊤`.
|
Mathlib.Data.Nat.PartENat._auxLemma.16
theorem Mathlib.Data.Nat.PartENat._auxLemma.16 : ∀ (x : ℕ), (↑x = ⊤) = False
This theorem states that for any natural number 'x', the expression '↑x = ⊤' is always false. Here, '↑x' denotes the lifting of the natural number 'x' to the extended natural numbers (including infinity, denoted by '⊤'). In other words, no natural number can be equal to infinity.
More concisely: The theorem asserts that for all natural numbers x, the lifted natural number ↑x is not equal to the top element ⊤.
|
PartENat.dom_of_le_natCast
theorem PartENat.dom_of_le_natCast : ∀ {x : PartENat} {y : ℕ}, x ≤ ↑y → x.Dom
This theorem states that for any partially defined natural number `x` and any fully defined natural number `y`, if `x` is less than or equal to the embedding of `y` into the type of partially defined natural numbers, then `x` is defined. In other words, it guarantees that `x` is not the infinity element in the set of partially defined natural numbers when it is less than or equal to a concrete natural number.
More concisely: If `x` is a partially defined natural number and `y` is a fully defined natural number such that `x ≤ embedding of y`, then `x` is defined.
|
PartENat.natCast_ne_top
theorem PartENat.natCast_ne_top : ∀ (x : ℕ), ↑x ≠ ⊤
This theorem states that for all natural numbers `x`, the cast of `x` to a different type cannot be equal to the top element `⊤`. In other words, it is not possible for any natural number to be cast to a type and result in the value that represents "everything" or "unbounded" in that type. This reflects an important constraint on type conversions in Lean.
More concisely: For all natural numbers x, the cast of x to any type cannot be the top element ⊤.
|
PartENat.toWithTop_natCast'
theorem PartENat.toWithTop_natCast' : ∀ (n : ℕ) {x : Decidable (↑n).Dom}, (↑n).toWithTop = ↑n
This theorem states that for all natural numbers `n`, and for all instances `x` where the domain of the coercive function `↑n` is decidable, the function `PartENat.toWithTop` applied to the coercive function `↑n` is equal to the coercive function `↑n` itself. In simpler terms, it's saying that the process of converting a partial extended natural number to a natural number with infinity, when applied to a natural number, essentially leaves the natural number unchanged.
More concisely: For all natural numbers `n` and decidable domains `X`, the coercion function `↑n : X → Nat` is equal to `PartENat.toWithTop ↑n`.
|
PartENat.natCast_lt_top
theorem PartENat.natCast_lt_top : ∀ (x : ℕ), ↑x < ⊤
This theorem states that for any natural number `x`, the real number representation (`↑x`) of `x` is less than positive infinity (`⊤`). In other words, no matter how large a natural number you have, it will always be less than positive infinity when considered as a real number.
More concisely: For all natural numbers x, ↑x < ⊤ in the real numbers.
|
Mathlib.Data.Nat.PartENat._auxLemma.2
theorem Mathlib.Data.Nat.PartENat._auxLemma.2 : ∀ (x : ℕ), (↑x).1 = True
This theorem, `Mathlib.Data.Nat.PartENat._auxLemma.2`, states that for every natural number `x`, the first component (`.1`) of the coe function applied to `x` (`↑x`) is equal to `True`. In other words, this theorem asserts that a certain condition holds true for the first component of the coe function when it is applied to any natural number.
More concisely: For every natural number `x`, the first component of the coe function of `x` is `True`. (or equivalently, the coe function of a natural number `x` is a pair where the first component is `True`)
|
Mathlib.Data.Nat.PartENat._auxLemma.23
theorem Mathlib.Data.Nat.PartENat._auxLemma.23 :
∀ {R : Type u_1} [inst : AddMonoidWithOne R] (m n : ℕ), ↑m + ↑n = ↑(m + n)
This theorem states that for any type `R` that is an additive monoid with an identity element (i.e., has operations for addition that follow the rules of an additive monoid and has a defined "one" element), the sum of the additive identities of two natural numbers `m` and `n` is equal to the additive identity of their sum. In other words, when `m` and `n` are interpreted (coerced) as elements of `R`, their sum in `R` is the same as if you first added them within the natural numbers and then interpreted the result as an element of `R`. This is written in LaTeX as: \( \forall R, m, n \in \mathbb{N}\), if `R` is an additive monoid with one, then \( m + n = m + n \) when both sides are considered as elements in `R`.
More concisely: For any additive monoid `R` with identity, the sum of two natural numbers `m` and `n` in `R` is equal to their sum in the natural numbers when interpreted as elements of `R`.
|
PartENat.ne_top_iff
theorem PartENat.ne_top_iff : ∀ {x : PartENat}, x ≠ ⊤ ↔ ∃ n, x = ↑n
This theorem states that for every object `x` of type `PartENat` (which is the type of natural numbers including infinity), `x` is not equal to infinity if and only if there exists a natural number `n` such that `x` is equal to the embedding of `n` into `PartENat`. In other words, a `PartENat` object is not infinity precisely when it is the embedding of a natural number.
More concisely: For every `PartENat` object `x`, `x` is finite if and only if there exists a natural number `n` such that `x` is equal to the embedding of `n` into `PartENat`.
|
PartENat.add_top
theorem PartENat.add_top : ∀ (x : PartENat), x + ⊤ = ⊤
This theorem states that for any element `x` of the type `PartENat`, which represents natural numbers along with the concept of infinity (`⊤`), the sum of `x` and infinity (`⊤`) is always infinity (`⊤`). Essentially, it encapsulates the mathematical idea that adding any number, even a potentially infinite one, to infinity still results in infinity.
More concisely: For any natural number `x` including infinity (⊤), `x + ⊤ = ⊤`.
|
PartENat.natCast_get
theorem PartENat.natCast_get : ∀ {x : PartENat} (h : x.Dom), ↑(x.get h) = x
This theorem states that for all partial natural numbers `x` with a defined domain, the natural number you get by applying the `get` function to `x` (assuming the domain `h` of `x` is defined) and then casting it to the type `PartENat`, is equal to `x` itself. In other words, it asserts that casting a retrieved value of a partial natural number back into the type of partial natural numbers doesn't change the original value.
More concisely: For all partial natural numbers `x` with a defined domain, `get x = PartENat.cast (get x)` holds.
|
PartENat.natCast_inj
theorem PartENat.natCast_inj : ∀ {x y : ℕ}, ↑x = ↑y ↔ x = y
This theorem states that for any two natural numbers `x` and `y`, the condition that their cast or conversion to `PartENat` (Partial Extended Natural numbers) are equal is equivalent to the condition that `x` and `y` themselves are equal. In other words, casting does not change the equality relation between natural numbers.
More concisely: For all natural numbers x and y, x = y if and only if (x : PartENat) = (y : PartENat).
|
PartENat.get_natCast'
theorem PartENat.get_natCast' : ∀ (x : ℕ) (h : (↑x).Dom), (↑x).get h = x
This theorem, `PartENat.get_natCast'`, states that for any natural number `x` and any proof `h` that `x` belongs to the domain of the embedding of natural numbers into partial extended natural numbers, accessing the value of the embedded number using `get` ultimately gives back `x`. Essentially, this theorem says that the process of embedding natural numbers into extended natural numbers and then retrieving them leaves the original number unchanged.
More concisely: For any natural number `x` and proof `h`, the embedding of `x` as a partial extended natural number and its retrieval using `get` equal `x`.
|
PartENat.dom_natCast
theorem PartENat.dom_natCast : ∀ (x : ℕ), (↑x).Dom
This theorem, `PartENat.dom_natCast`, asserts that for every natural number `x`, the domain of the cast of `x` to a partial extended natural number (as represented by `(↑x).Dom`) is well-defined. In other words, you can always cast a natural number to a partial extended natural number.
More concisely: For every natural number x, the cast of x to a partial extended natural number is a defined value.
|
Mathlib.Data.Nat.PartENat._auxLemma.24
theorem Mathlib.Data.Nat.PartENat._auxLemma.24 : ∀ {b : Prop} (α : Sort u_1) [i : Nonempty α], (α → b) = b
This theorem states that for any proposition `b` and any type `α` that is nonempty (i.e., has at least one value), the type of functions from `α` to `b` is equivalent to `b` itself. In other words, regardless of what `α` is, if there is at least one value of type `α`, then a function that takes an input of type `α` and outputs a proposition `b` is itself effectively a proposition `b`. This reflects the intuition that if there's only one possibility for an input, then a function depending on that input is essentially the same as its output.
More concisely: For any nonempty type `α`, the type of functions from `α` to a proposition `b` is equivalent to `b`.
|
PartENat.le_of_lt_add_one
theorem PartENat.le_of_lt_add_one : ∀ {x y : PartENat}, x < y + 1 → x ≤ y
This theorem states that for any two elements `x` and `y` of the type `PartENat` (which represents natural numbers with an additional element representing infinity), if `x` is less than `y + 1`, then `x` is also less than or equal to `y`. This is a commonly understood property in the domain of natural numbers and extends appropriately to this extended number system that includes infinity.
More concisely: For any `x` and `y` in `PartENat`, if `x < y + 1`, then `x ≤ y`.
|