Nat.compare_def_lt
theorem Nat.compare_def_lt :
∀ (a b : ℕ), compare a b = if a < b then Ordering.lt else if b < a then Ordering.gt else Ordering.eq
This theorem, `Nat.compare_def_lt`, states that for any two natural numbers `a` and `b`, the comparison of `a` and `b` is defined as follows: if `a` is less than `b`, then the result of the comparison is `Ordering.lt` (less than); if `b` is less than `a`, then the result is `Ordering.gt` (greater than); and if neither of these cases is true (that is, `a` and `b` are equal), then the result is `Ordering.eq` (equal).
More concisely: For all natural numbers `a` and `b`, `a` < `b` if and only if `Ordering.lt` is the result of comparing `a` and `b`, while `a` > `b` if and only if `Ordering.gt` is the result, and `a` = `b` if and only if `Ordering.eq` is the result.
|
Nat.compare_def_le
theorem Nat.compare_def_le :
∀ (a b : ℕ), compare a b = if a ≤ b then if b ≤ a then Ordering.eq else Ordering.lt else Ordering.gt
This theorem states that for any two natural numbers `a` and `b`, the comparison operation `compare a b` is defined as follows: if `a` is less than or equal to `b`, then check if `b` is less than or equal to `a`; if it is, then `a` and `b` are equal (`Ordering.eq`), otherwise `a` is less than `b` (`Ordering.lt`). If `a` is not less than or equal to `b`, then `a` is greater than `b` (`Ordering.gt`).
More concisely: For all natural numbers `a` and `b`, `compare a b` is `Ordering.eq` if and only if `a` is less than or equal to `b` and `b` is less than or equal to `a`, and `compare a b` is `Ordering.lt` if and only if `a` is less than `b` and `b` is greater than or equal to `a`.
|