Nat.dist_eq_sub_of_le_right
theorem Nat.dist_eq_sub_of_le_right : ∀ {n m : ℕ}, m ≤ n → n.dist m = n - m
This theorem states that for any two natural numbers `n` and `m`, if `m` is less than or equal to `n`, then the distance between `n` and `m`, as defined by the `Nat.dist` function, is equal to the difference `n - m`. This means that when `m` is less than or equal to `n`, the distance between these two numbers is simply the subtraction of `m` from `n` in the set of natural numbers.
More concisely: For all natural numbers `n` and `m`, `Nat.dist n m = n - m` when `m ≤ n`.
|
Nat.dist_comm
theorem Nat.dist_comm : ∀ (n m : ℕ), n.dist m = m.dist n
The theorem `Nat.dist_comm` states that for all natural numbers `n` and `m`, the distance between `n` and `m` is the same as the distance between `m` and `n`. This expresses the commutative property of the distance function on natural numbers, which implies that the order of the inputs does not affect the result: swapping the inputs will yield the same output. In mathematical notation, we can write this as: for all $n, m \in \mathbb{N}$, $\text{dist}(n, m) = \text{dist}(m, n)$.
More concisely: The distance between any two natural numbers is commutative, i.e., dist(n, m) = dist(m, n) for all natural numbers n and m.
|
Nat.dist_eq_sub_of_le
theorem Nat.dist_eq_sub_of_le : ∀ {n m : ℕ}, n ≤ m → n.dist m = m - n
This theorem states that for any two natural numbers `n` and `m`, if `n` is less than or equal to `m`, then the distance between `n` and `m`, as defined by the `Nat.dist` function, is equal to the difference between `m` and `n`. In other words, if `n` is less than or equal to `m`, then the absolute value of the difference between `n` and `m` is simply `m - n`.
More concisely: For all natural numbers `n` and `m`, `Nat.dist n m = m - n` when `n ≤ m`.
|