Nat.succPNat_strictMono
theorem Nat.succPNat_strictMono : StrictMono Nat.succPNat
The theorem `Nat.succPNat_strictMono` states that the function `Nat.succPNat`, which maps a natural number to its successor represented as a positive natural number, is strictly monotone. In other words, if `a` and `b` are two natural numbers and `a < b`, then the successor of `a` represented as a positive natural number is less than the successor of `b` represented as a positive natural number.
More concisely: The function `Nat.succPNat` strictly increases natural numbers, i.e., for all `a` and `b` in `Nat`, if `a < b`, then `Nat.succPNat a < Nat.succPNat b`.
|
PNat.coe_inj
theorem PNat.coe_inj : ∀ {m n : ℕ+}, ↑m = ↑n ↔ m = n
This theorem, `PNat.coe_inj`, states that for any two positive natural numbers `m` and `n`, the coercion of `m` and `n` to natural numbers are equal if and only if `m` and `n` themselves are equal. In other words, the process of converting positive natural numbers to natural numbers (using the coercion function `↑`) preserves their equality.
More concisely: For all natural numbers `m` and `n`, `↑m = ↑n` if and only if `m = n`.
|
PNat.pow_coe
theorem PNat.pow_coe : ∀ (m : ℕ+) (n : ℕ), ↑(m ^ n) = ↑m ^ n
This theorem states that for every positive natural number `m` and every natural number `n`, the process of first raising `m` to the power of `n` and then taking the result to the domain of natural numbers is equivalent to first taking `m` to the domain of natural numbers and then raising it to the power of `n`. In mathematical notation, this can be written as: ∀m∈ℕ+ and ∀n∈ℕ, (m^n) = m^n.
More concisely: For all natural numbers `m` and `n`, raising `m` to the power of `n` in the domain of natural numbers is equal to first taking `m` to the domain of natural numbers and then raising it to the power of `n`. In mathematical notation, `(m^n) = m^n` for all `m ∈ ℕ+` and `n ∈ ℕ`.
|
PNat.dvd_iff
theorem PNat.dvd_iff : ∀ {k m : ℕ+}, k ∣ m ↔ ↑k ∣ ↑m
This theorem states that for any two positive natural numbers `k` and `m`, `k` divides `m` if and only if the coercive of `k` (i.e., `k` treated as a natural number) divides the coercive of `m` (i.e., `m` treated as a natural number). It is a way to connect the divisibility relationship in the domain of positive natural numbers with that in the domain of natural numbers.
More concisely: For all natural numbers `k` and `m`, `k` divides `m` if and only if the natural number `k` divides the natural number `m`.
|
PNat.exists_eq_succ_of_ne_one
theorem PNat.exists_eq_succ_of_ne_one : ∀ {n : ℕ+}, n ≠ 1 → ∃ k, n = k + 1
This theorem states that for any positive natural number `n` that is not equal to `1`, there exists another positive natural number `k` such that `n` is the successor of `k`. In other words, if a positive natural number is not `1`, then it can be expressed as `k + 1` for some positive natural number `k`.
More concisely: For every positive natural number `n` different from `1`, there exists a natural number `k` such that `n = Suc(k)`. (Here, `Suc` denotes the successor function.)
|
PNat.natPred_strictMono
theorem PNat.natPred_strictMono : StrictMono PNat.natPred
The theorem `PNat.natPred_strictMono` states that the function `PNat.natPred`, which calculates the predecessor of a positive natural number (turns it into a natural number), is strictly monotone. This means that for any two distinct positive natural numbers `a` and `b`, if `a` is less than `b`, then `PNat.natPred a` is also less than `PNat.natPred b`.
More concisely: The function `PNat.natPred` strictly decreases positive natural numbers, i.e., for all distinct `a` and `b` in `PNat` with `a < b`, `PNat.natPred a < P Nat.natPred b`.
|
PNat.mul_coe
theorem PNat.mul_coe : ∀ (m n : ℕ+), ↑(m * n) = ↑m * ↑n
This theorem states that for any two positive natural numbers `m` and `n`, the positive natural number obtained by multiplying `m` and `n` (denoted by `m * n`) is the same as the integer obtained by first converting `m` and `n` to integers (denoted by `↑m` and `↑n`) and then multiplying them. Essentially, multiplying the positive natural numbers first and then converting to an integer gives the same result as converting to integers first and then multiplying.
More concisely: For any natural numbers m and n, (m * n) = (↑m * ↑n).
|