CovBy.cast_int
theorem CovBy.cast_int : ∀ {a b : ℕ}, a ⋖ b → ↑a ⋖ ↑b
This theorem, `CovBy.cast_int`, states that for any two natural numbers `a` and `b`, if `a` is covered by `b` (denoted as `a ⋖ b`), then the integer cast of `a` is also covered by the integer cast of `b` (denoted as `↑a ⋖ ↑b`). In other words, the property of being "covered by" is preserved when the natural numbers are cast to integers.
More concisely: For all natural numbers `a` and `b`, if `a` is covered by `b` (`a ⋖ b`), then the integer cast of `a` (`↑a`) is covered by the integer cast of `b` (`↑b`).
|
Int.covBy_iff_succ_eq
theorem Int.covBy_iff_succ_eq : ∀ {m n : ℤ}, m ⋖ n ↔ m + 1 = n
This theorem states that for any two integers `m` and `n`, `m` is covered by `n` (denoted `m ⋖ n`) if and only if `m + 1` is equal to `n`. In other words, an integer `m` is considered to be covered by another integer `n` precisely when `n` is the next integer following `m`.
More concisely: For integers `m` and `n`, `m ⋖ n` holds if and only if `m + 1 = n`.
|