Rat.toNNRat.proof_1
theorem Rat.toNNRat.proof_1 : ∀ (q : ℚ), 0 ≤ max q 0
This theorem states that for any rational number `q`, the maximum of `q` and `0` is always non-negative. This makes sense, as the maximum of a given rational number and zero would either be that rational number (if it is positive) or zero (if the rational number is negative or zero), both of which are non-negative numbers.
More concisely: For any rational number q, 0 ≤ q max 0.
|
NNRat.coe_inj
theorem NNRat.coe_inj : ∀ {p q : ℚ≥0}, ↑p = ↑q ↔ p = q
This theorem, `NNRat.coe_inj`, asserts that for any two nonnegative rational numbers `p` and `q`, the equality of their coercions (i.e., treating them as regular rational numbers) implies the equality of `p` and `q` themselves. In other words, no two different nonnegative rational numbers can be interpreted as the same rational number. This is the statement of injectivity for the coercion from `NNRat` to `Rat`.
More concisely: For all nonnegative rational numbers p and q, if p = (rat.coerce p) = (rat.coerce q), then p = q.
|
NNRat.coe_le_coe
theorem NNRat.coe_le_coe : ∀ {p q : ℚ≥0}, ↑p ≤ ↑q ↔ p ≤ q
This theorem states that for any two nonnegative rational numbers `p` and `q` (represented by `NNRat`), the standard mathematical inequality `p ≤ q` holds true if and only if the inequality `↑p ≤ ↑q` also holds true when `p` and `q` are coerced (or converted) into another type that supports the comparison (like real numbers or rational numbers for instance). In other words, the comparison of the nonnegative rational numbers is preserved under coercion.
More concisely: For any nonnegative rational numbers `p` and `q`, `p ≤ q` if and only if `↑p ≤ ↑q`, where `↑` denotes coercion to a type that supports comparison.
|
Rat.coe_toNNRat
theorem Rat.coe_toNNRat : ∀ (q : ℚ), 0 ≤ q → ↑q.toNNRat = q
This theorem asserts that for any rational number `q`, if `q` is non-negative (i.e., `q` is greater than or equal to zero), then converting `q` to a non-negative rational number using the function `Rat.toNNRat` and then converting it back to a regular rational number yields the original value `q`. In mathematical terms, it states that for all `q` in the set of rational numbers, `ℚ`, such that `0 ≤ q`, the function `Rat.toNNRat` is effectively an identity operation.
More concisely: For all non-negative rational numbers `q`, `Rat.toNNRat q = q`.
|
Rat.toNNRat_eq_zero
theorem Rat.toNNRat_eq_zero : ∀ {q : ℚ}, q.toNNRat = 0 ↔ q ≤ 0
This theorem states that for any rational number 'q', the function `Rat.toNNRat` that maps 'q' to a non-negative rational number returns 0 if and only if 'q' is less than or equal to 0. This means the conversion of 'q' to a non-negative rational number will yield 0 precisely when 'q' is not positive.
More concisely: For any rational number q, Rat.toNNRat q = 0 if and only if q ≤ 0.
|
NNRat.ext
theorem NNRat.ext : ∀ {p q : ℚ≥0}, ↑p = ↑q → p = q
This theorem, `NNRat.ext`, states that for any two nonnegative rational numbers `p` and `q`, if these numbers are equal when coerced to their underlying rational numbers (i.e., `↑p = ↑q`), then `p` and `q` themselves are also equal. It is essentially stating that the equality in the universe of nonnegative rational numbers (`NNRat`) is consistent with the equality in the universe of all rational numbers.
More concisely: For any nonnegative rational numbers `p` and `q`, if `↑p = ↑q`, then `p = q`.
|
Rat.toNNRat_of_nonpos
theorem Rat.toNNRat_of_nonpos : ∀ {q : ℚ}, q ≤ 0 → q.toNNRat = 0
This theorem states that for any rational number `q`, if `q` is less than or equal to zero, then the non-negative rational representation of `q` is zero. In other words, converting a non-positive rational number to a non-negative rational number results in zero.
More concisely: For any rational number `q`, if `q` is non-positive then its non-negative rational representation is zero.
|