PNat.mk_le_mk
theorem PNat.mk_le_mk : ∀ (n k : ℕ) (hn : 0 < n) (hk : 0 < k), ⟨n, hn⟩ ≤ ⟨k, hk⟩ ↔ n ≤ k
This theorem establishes the relationship between the less than or equal to (`≤`) operation on positive natural numbers (`ℕ+`) and natural numbers (`ℕ`). Specifically, for any two natural numbers `n` and `k` that are greater than zero, the statement that `n` is less than or equal to `k` is equivalent to the statement that the corresponding positive natural numbers, represented as `⟨n, hn⟩` and `⟨k, hk⟩`, have the same order relation. That is, `⟨n, hn⟩ ≤ ⟨k, hk⟩` if and only if `n ≤ k`.
More concisely: For any natural numbers `n` and `k` greater than zero, `n ≤ k` if and only if `⟨n, hn⟩ ≤ ⟨k, hk⟩` in the ordering of positive natural numbers.
|
PNat.pos
theorem PNat.pos : ∀ (n : ℕ+), 0 < ↑n
This theorem states that for every positive natural number `n`, the value of `n` when coerced to an integer is strictly greater than zero. In other words, when we take any positive natural number and view it as an integer, the result is always a positive integer.
More concisely: For every natural number n, the integer coercion of n is positive.
|
Mathlib.Data.PNat.Defs._auxLemma.3
theorem Mathlib.Data.PNat.Defs._auxLemma.3 : ∀ (n : ℕ+), (0 < ↑n) = True
This theorem, `Mathlib.Data.PNat.Defs._auxLemma.3`, states that for all positive natural numbers `n` (denoted as `ℕ+`), the condition that `n` is greater than zero is always true. This result is expected because by definition, positive natural numbers are always greater than zero.
More concisely: For all positive natural numbers `n`, `n` is greater than zero.
|
PNat.eq
theorem PNat.eq : ∀ {m n : ℕ+}, ↑m = ↑n → m = n
This theorem asserts that for any two positive natural numbers `m` and `n`, if their cast to natural numbers are equal, then `m` and `n` themselves are also equal. In mathematical terms, for all `m, n` in `ℕ+`, if `m` cast to `ℕ` equals `n` cast to `ℕ`, then `m` equals `n`.
More concisely: For all natural numbers `m` and `n`, if `m` = (cast `m` to `ℕ`) = (cast `n` to `ℕ`) then `m` = `n`.
|
PNat.toPNat'_coe
theorem PNat.toPNat'_coe : ∀ {n : ℕ}, 0 < n → ↑n.toPNat' = n
This theorem states that for any natural number `n`, given the condition that `n` is greater than 0, the function `Nat.toPNat'` converts `n` to a positive natural number, and when this result is then converted back to a natural number, we get `n` back. In other words, the function `Nat.toPNat'` acts as an identity function when applied to any natural number greater than 0, preserving the initial value through the conversion processes.
More concisely: For any natural number `n` greater than 0, `Nat.toPNat'` and its inverse conversion function yield `n`. In mathematical notation: `(Nat.toPNat' ∘ Nat.cast) (n : Nat) = n` where `Nat.cast` is the conversion from positive natural number to natural number.
|
Mathlib.Data.PNat.Defs._auxLemma.4
theorem Mathlib.Data.PNat.Defs._auxLemma.4 : ∀ (n : ℕ+), (↑n = 0) = False
This theorem, `Mathlib.Data.PNat.Defs._auxLemma.4`, states that for any positive natural number `n`, the predicate that `n` equals zero is always false. In other words, it means that no positive natural number can be zero. The `Nat+` refers to the set of positive natural numbers, and `n` is a member of this set. The `↑n = 0` is the predicate under consideration, where `↑n` is the operation of embedding `n` into the naturals (which doesn't change its value), and `0` is the natural number zero.
More concisely: For any positive natural number `n`, the predicate `n = 0` is false.
|
PNat.one_le
theorem PNat.one_le : ∀ (n : ℕ+), 1 ≤ n
The theorem `PNat.one_le` states that for all positive natural numbers `n` (`ℕ+`), `n` is greater than or equal to 1. That is, no positive natural number is less than 1.
More concisely: For all natural numbers `n`, `1 ≤ n`.
|
PNat.ne_zero
theorem PNat.ne_zero : ∀ (n : ℕ+), ↑n ≠ 0
This theorem states that for every positive natural number `n`, the integer representation of `n` is not equal to zero. In other words, there is no positive natural number that equals zero when converted to an integer.
More concisely: For every positive natural number `n`, 0 ≠Int. n.
|
PNat.one_coe
theorem PNat.one_coe : ↑1 = 1
This theorem states that the natural number representation of 1 is equal to 1. In other words, the coercion function (^^) applied to the positive integer 1 results in the natural number 1. This is a basic property of numbers and their representations in Lean 4.
More concisely: The theorem asserts that the coercion of the constant 1 to the type of natural numbers results in the natural number 1. In mathematical notation, `1 ^^ = 1`.
|