Int.sub_pos_of_lt
theorem Int.sub_pos_of_lt : ∀ {a b : ℤ}, b < a → 0 < a - b
This theorem states that for any two integers `a` and `b`, if `b` is less than `a`, then the result of `a - b` is greater than zero. In other words, subtracting a smaller integer from a larger integer will always give a positive result.
More concisely: For all integers `a` and `b` with `b < a`, `a - b` is positive.
|
Int.eq_negSucc_of_lt_zero
theorem Int.eq_negSucc_of_lt_zero : ∀ {a : ℤ}, a < 0 → ∃ n, a = Int.negSucc n
This theorem states that for any integer `a`, if `a` is less than zero, then there exists a natural number `n` such that `a` is equal to the negative of the successor of `n` (i.e. `a = -n - 1`). In essence, it is expressing the fact that every negative integer is the negative of the successor of some natural number.
More concisely: For any integer `a` less than zero, there exists a natural number `n` such that `a = -(Suc n)`, where `Suc` denotes the successor operation.
|
Int.le_add_of_nonneg_right
theorem Int.le_add_of_nonneg_right : ∀ {a b : ℤ}, 0 ≤ b → a ≤ a + b
This theorem states that for any two integers `a` and `b`, if `b` is non-negative (i.e., `b` is greater than or equal to zero), then `a` is less than or equal to the sum of `a` and `b`. Intuitively, adding a non-negative number to `a` will not make `a` smaller; it will either stay the same (if `b` is zero) or become larger.
More concisely: For all integers `a` and `b`, if `b` is non-negative then `a` is less than or equal to `a + b`.
|
Int.eq_ofNat_of_zero_le
theorem Int.eq_ofNat_of_zero_le : ∀ {a : ℤ}, 0 ≤ a → ∃ n, a = ↑n
This theorem states that for any integer 'a', if 'a' is greater than or equal to zero, then there exists a natural number 'n' such that 'a' is equal to the integer representation of 'n'. In other words, any non-negative integer can be expressed as the integer representation of some natural number.
More concisely: For any non-negative integer `a`, there exists a natural number `n` such that `a = Nat.toInt n`.
|
Int.le_refl
theorem Int.le_refl : ∀ (a : ℤ), a ≤ a
This theorem states that for any integer `a`, `a` is less than or equal to itself. In mathematical terms, this is known as reflexivity of the less than or equal relationship over the set of integers (`ℤ`), and it is a fundamental property of the ordering of numbers.
More concisely: For all integers `a`, `a` is less than or equal to `a` (`∀ a : ℤ, a ≤ a`).
|
Int.sub_left_le_of_le_add
theorem Int.sub_left_le_of_le_add : ∀ {a b c : ℤ}, a ≤ b + c → a - b ≤ c
This theorem, named `Int.sub_left_le_of_le_add`, expresses a relation between integers `a`, `b`, and `c`. It states that for any integers `a`, `b`, and `c`, if `a` is less than or equal to the sum of `b` and `c` (expressed as `a ≤ b + c`), then `a` minus `b` is less than or equal to `c` (expressed as `a - b ≤ c`). This is a basic property arising from the arithmetic of integers.
More concisely: If `a` is less than or equal to `b + c` for integers `a`, `b`, and `c`, then `a - b` is less than or equal to `c`.
|
Int.lt_of_not_ge
theorem Int.lt_of_not_ge : ∀ {a b : ℤ}, ¬a ≤ b → b < a
This theorem, known as `Int.lt_of_not_ge`, is an alias for the forward direction of `Int.not_le`. It states that for any two integers `a` and `b`, if `a` is not less than or equal to `b`, then `b` must be less than `a`. This is a basic property of integer comparison in mathematics.
More concisely: If `a` is not less than or equal to `b` (`a >= b` is false), then `b` is less than `a` (`b < a`).
|
Int.le.dest_sub
theorem Int.le.dest_sub : ∀ {a b : ℤ}, a ≤ b → ∃ n, b - a = ↑n
This theorem states that for any two integer values 'a' and 'b', if 'a' is less than or equal to 'b', then there exists a natural number 'n' such that the difference of 'b' and 'a' is equal to 'n'. In other words, every nonnegative difference between two integers can be expressed as a natural number.
More concisely: For any integers 'a' and 'b' with 'a' ≤ 'b', there exists a natural number 'n' such that 'b' = 'a' + 'n'.
|
Int.lt_of_le_of_lt
theorem Int.lt_of_le_of_lt : ∀ {a b c : ℤ}, a ≤ b → b < c → a < c
This theorem states that for any three integers `a`, `b`, and `c`, if `a` is less than or equal to `b`, and `b` is strictly less than `c`, then `a` is strictly less than `c`. It captures the transitivity property of the "less than" relation over integers: being less than or equal to an integer which is in turn less than another integer implies being less than the latter integer.
More concisely: If `a` is less than or equal to `b` and `b` is strictly less than `c`, then `a` is strictly less than `c`. (In other words, transitivity holds for the strict less than relation on integers.)
|
Int.add_le_of_le_sub_right
theorem Int.add_le_of_le_sub_right : ∀ {a b c : ℤ}, a ≤ c - b → a + b ≤ c
This theorem states that for all integers `a`, `b`, and `c`, if `a` is less than or equal to `c - b`, then `a + b` is less than or equal to `c`. In terms of mathematical notation, this would be expressed as ∀a, b, c ∈ ℤ, if a ≤ c - b, then a + b ≤ c. This is a property of integer arithmetic and inequality.
More concisely: For all integers `a`, `b`, and `c`, if `a ≤ c - b`, then `a + b ≤ c`.
|
Int.neg_nonneg_of_nonpos
theorem Int.neg_nonneg_of_nonpos : ∀ {a : ℤ}, a ≤ 0 → 0 ≤ -a
This theorem states that for any integer `a`, if `a` is less than or equal to zero, then the negative of `a` is greater than or equal to zero. In other words, if `a` is non-positive (i.e., it's either negative or zero), then `-a` is non-negative (i.e., it's either positive or zero). This corresponds to the familiar mathematical fact that the negation of a non-positive number is a non-negative number.
More concisely: For any integer `a`, if `a` is non-positive, then -`a` is non-negative.
|
Int.le_of_lt
theorem Int.le_of_lt : ∀ {a b : ℤ}, a < b → a ≤ b
This theorem, `Int.le_of_lt`, states that for any two integer values `a` and `b`, if `a` is strictly less than `b`, then `a` is also less than or equal to `b`. In mathematical terms, if a < b, it implies that a ≤ b. This theorem is generally applicable in the field of integer numbers.
More concisely: For all integers a and b, if a < b then a ≤ b.
|
Int.mul_pos
theorem Int.mul_pos : ∀ {a b : ℤ}, 0 < a → 0 < b → 0 < a * b
This theorem states that for any two integers `a` and `b`, if both `a` and `b` are greater than zero, then their product is also greater than zero. In other words, the product of two positive integers is always a positive integer.
More concisely: For all integers `a` and `b` > 0, their product `a * b` is also positive.
|
Int.natAbs_eq
theorem Int.natAbs_eq : ∀ (a : ℤ), a = ↑a.natAbs ∨ a = -↑a.natAbs
The theorem `Int.natAbs_eq` states that for every integer `a`, `a` is equal to the absolute value of `a` (which is a natural number) or `a` is equal to the negation of the absolute value of `a`. In other words, an integer is either its own absolute value or its negative. Essentially, this theorem reflects that the absolute value function in integers returns the magnitude of the integer without regard to its sign.
More concisely: For every integer `a`, `|a| = a` or `|a| = -a`.
|
Int.not_le
theorem Int.not_le : ∀ {a b : ℤ}, ¬a ≤ b ↔ b < a
This theorem states that for all integers `a` and `b`, `a` is not less than or equal to `b` if and only if `b` is strictly less than `a`. In mathematical terms, it illustrates the antecedent relationship between the negation of the "less than or equal to" comparison and the "strictly less than" comparison for integers.
More concisely: For integers `a` and `b`, `a` is not less than or equal to `b` if and only if `b` is strictly less than `a`. In Lean, this can be expressed as `∀ (a b : ℤ), a ≤ b ��ври b < a`.
|
Int.not_lt
theorem Int.not_lt : ∀ {a b : ℤ}, ¬a < b ↔ b ≤ a
This theorem states that for any two integers 'a' and 'b', 'a' is not less than 'b' if and only if 'b' is less than or equal to 'a'. In other words, if 'a' is not less than 'b', then 'b' must be less than or equal to 'a', and vice versa. The theorem represents a basic property of ordering in the set of integers.
More concisely: For all integers a and b, a ≤ b if and only if not (a < b).
|
Int.neg_pos_of_neg
theorem Int.neg_pos_of_neg : ∀ {a : ℤ}, a < 0 → 0 < -a
This theorem, `Int.neg_pos_of_neg`, states that for any integer `a`, if `a` is less than zero (i.e., `a` is a negative integer), then the negative of `a` is greater than zero. In other words, negating a negative integer results in a positive integer. This is a basic property of integers in number theory.
More concisely: For any integer `a`, if `a` is negative then -`a` is positive.
|
Int.natAbs_of_nonneg
theorem Int.natAbs_of_nonneg : ∀ {a : ℤ}, 0 ≤ a → ↑a.natAbs = a
This theorem states that for every integer `a`, if `a` is nonnegative (i.e., `a` is greater than or equal to zero), then the absolute value of `a` as a natural number (i.e., `Int.natAbs a`) when converted back to an integer equals to `a` itself. The function `Int.natAbs` is used to find the absolute value of `a` and the upward arrow symbol (`↑`) is used for type coercion, converting the natural number back to an integer.
More concisely: For every integer `a` greater than or equal to zero, `Int.natAbs a = ↑a`.
|
Int.ne_of_lt
theorem Int.ne_of_lt : ∀ {a b : ℤ}, a < b → a ≠ b
This theorem states that for any two integers `a` and `b`, if `a` is less than `b`, then `a` is not equal to `b`. Essentially, it asserts the inconsistency of an integer being simultaneously less than and equal to another specific integer.
More concisely: For all integers a and b, if a < b then a ≠ b.
|
Int.add_le_add_right
theorem Int.add_le_add_right : ∀ {a b : ℤ}, a ≤ b → ∀ (c : ℤ), a + c ≤ b + c
This theorem states that for any three integer values `a`, `b`, and `c`, if `a` is less than or equal to `b`, then the sum of `a` and `c` is also less than or equal to the sum of `b` and `c`. This is also known as the principle of preserving order under addition in the integers.
More concisely: For all integers a, b, and c, if a ≤ b then a + c ≤ b + c.
|
Int.ofNat_natAbs_of_nonpos
theorem Int.ofNat_natAbs_of_nonpos : ∀ {a : ℤ}, a ≤ 0 → ↑a.natAbs = -a
The theorem `Int.ofNat_natAbs_of_nonpos` states that for any integer `a` which is less than or equal to zero, the absolute value (represented as a natural number) of `a` when converted back to an integer equals the negative of `a`. In other words, for any non-positive integer, its absolute value behaves as if we removed the negative sign, and this relationship holds when we convert this absolute value back to an integer.
More concisely: For any integer `a`, if `a` is non-positive, then |a| = -a.
|
Int.lt_add_one_iff
theorem Int.lt_add_one_iff : ∀ {a b : ℤ}, a < b + 1 ↔ a ≤ b
This theorem, `Int.lt_add_one_iff`, is a statement about integer inequality. For all integers `a` and `b`, the theorem states that `a` is less than `b + 1` if and only if `a` is less than or equal to `b`. This theorem bridges the relational gap between less than and less than or equal, and demonstrates an interesting property of integer arithmetic.
More concisely: For all integers `a` and `b`, `a` < `b` if and only if `a` <= `b` + 1.
|
Int.natAbs_pos
theorem Int.natAbs_pos : ∀ {a : ℤ}, 0 < a.natAbs ↔ a ≠ 0
This theorem states that for any integer `a`, the absolute value of `a` (denoted `Int.natAbs a`) is greater than zero if and only if `a` is not equal to zero. In other words, the absolute value of an integer is positive precisely when that integer is non-zero.
More concisely: For any integer `a`, `Int.natAbs a > 0` if and only if `a` is non-zero.
|
Int.le.intro_sub
theorem Int.le.intro_sub : ∀ {a b : ℤ} (n : ℕ), b - a = ↑n → a ≤ b
This theorem, named `Int.le.intro_sub`, states that for any pair of integers `a` and `b`, and a natural number `n`, if the difference `b - a` is equal to the natural number `n` (represented as an integer), then `a` is less than or equal to `b`. This is basically an introductory theorem for proving the less than or equal operation in the context of subtracting an integer from another.
More concisely: If an integer `a` is less than or equal to another integer `b`, then `b` minus `a` is a natural number.
|
Int.toNat_of_nonneg
theorem Int.toNat_of_nonneg : ∀ {a : ℤ}, 0 ≤ a → ↑a.toNat = a
This theorem states that for every integer `a`, if `a` is nonnegative (i.e., `a` is greater than or equal to 0), then converting `a` to a natural number using the function `Int.toNat` and then converting it back to an integer (indicated by `↑`) gives you `a` back. In essence, for nonnegative integers, the functions `Int.toNat` and then integer conversion form an identity operation.
More concisely: For every non-negative integer `a`, `Int.toNat a = a` holds.
|
Int.add_lt_add
theorem Int.add_lt_add : ∀ {a b c d : ℤ}, a < b → c < d → a + c < b + d
This theorem states that for any four integers `a`, `b`, `c`, and `d`, if `a` is less than `b` and `c` is less than `d`, then the sum of `a` and `c` is less than the sum of `b` and `d`. This is a property of integer addition and comparison, asserting that the order of the numbers is preserved when adding two pairs of integers where each pair has a smaller and a larger number.
More concisely: For all integers a, b, c, and d, if a < b and c < d then a + c < b + d.
|
Int.lt_of_lt_of_le
theorem Int.lt_of_lt_of_le : ∀ {a b c : ℤ}, a < b → b ≤ c → a < c
This theorem states that for any three integers `a`, `b`, and `c`, if `a` is less than `b` and `b` is less than or equal to `c`, then `a` is less than `c`. It's essentially a statement of the transitivity of the less-than relation under certain constraints.
More concisely: If `a` < `b` and `b` <= `c`, then `a` < `c`. (Transitivity of the less-than relation under constraints `a` < `b` and `b` <= `c`)
|
Int.lt_of_neg_lt_neg
theorem Int.lt_of_neg_lt_neg : ∀ {a b : ℤ}, -b < -a → a < b
This theorem, `Int.lt_of_neg_lt_neg`, states that for any two integers `a` and `b`, if the negation of `b` is less than the negation of `a` (i.e., `-b < -a`), then `a` is less than `b` (i.e., `a < b`). This theorem is a reflection of the property in number theory that reversing the order of inequality holds when both sides are negated.
More concisely: For all integers `a` and `b`, `-a < -b` implies `b < a`.
|
Int.lt_iff_le_and_ne
theorem Int.lt_iff_le_and_ne : ∀ {a b : ℤ}, a < b ↔ a ≤ b ∧ a ≠ b
This theorem states that for any two integers `a` and `b`, `a` is less than `b` if and only if `a` is less than or equal to `b` and `a` is not equal to `b`. In other words, the "<" relation on integers is completely determined by the "≤" relation and the "≠" relation.
More concisely: For integers `a` and `b`, `a` < `b` if and only if `a` ≤ `b` and `a` ≠ `b`.
|
Int.natAbs_one
theorem Int.natAbs_one : Int.natAbs 1 = 1
The theorem `Int.natAbs_one` states that the absolute value of 1, when considered as an integer, is equal to 1. This is intuitive as the absolute value of any number, which is defined as its distance from zero along the number line, is always non-negative. In particular, the absolute value of 1 is 1 itself.
More concisely: The theorem `Int.natAbs_one` asserts that |1| = 1 in the context of integers.
|
Int.lt_trichotomy
theorem Int.lt_trichotomy : ∀ (a b : ℤ), a < b ∨ a = b ∨ b < a
This theorem, "Int.lt_trichotomy", states that for any two integers `a` and `b`, exactly one of the following is true: `a` is less than `b`, `a` is equal to `b`, or `b` is less than `a`. This is essentially the principle of trichotomy for integers, a basic property of ordered fields.
More concisely: For any integers `a` and `b`, exactly one of `a < b`, `a = b`, or `b < a` holds.
|
Int.natAbs_eq_zero
theorem Int.natAbs_eq_zero : ∀ {a : ℤ}, a.natAbs = 0 ↔ a = 0
The theorem `Int.natAbs_eq_zero` states that for any integer `a`, the absolute value of `a` is equal to zero if and only if `a` itself is zero. In other words, the absolute value operation (`Int.natAbs`) on an integer value results in zero exactly when the original integer value is zero. This is a two-way implication, meaning if `a` is zero, then its absolute value is zero and vice versa.
More concisely: For all integers a, |a| = 0 if and only if a = 0.
|
Int.le_max_left
theorem Int.le_max_left : ∀ (a b : ℤ), a ≤ max a b
This theorem, `Int.le_max_left`, states that for any two integers `a` and `b`, `a` is less than or equal to the maximum of `a` and `b`. In other words, no matter what two integers you choose, the first integer will always be less than or equal to whichever one is larger.
More concisely: For all integers a and b, a <= max a b.
|
Int.not_le_of_gt
theorem Int.not_le_of_gt : ∀ {a b : ℤ}, b < a → ¬a ≤ b
This theorem, `Int.not_le_of_gt`, is essentially an alias for the reverse direction of the `Int.not_le` theorem. It states that for any two integers `a` and `b`, if `b` is less than `a` then it is not true that `a` is less than or equal to `b`. In mathematical terms, if b < a, then it is not the case that a ≤ b.
More concisely: For all integers a and b, if b < a then a > b.
|
Int.mul_le_mul_of_nonneg_left
theorem Int.mul_le_mul_of_nonneg_left : ∀ {a b c : ℤ}, a ≤ b → 0 ≤ c → c * a ≤ c * b
This theorem states that for any three integers `a`, `b`, and `c`, if `a` is less than or equal to `b` and `c` is non-negative (i.e., `c` is greater than or equal to 0), then the product of `c` and `a` is less than or equal to the product of `c` and `b`. In other words, in the context of integers, multiplication preserves the order of non-negative numbers.
More concisely: For integers `a`, `b`, and `c` with `a ≤ b` and `c ≥ 0`, we have `c * a ≤ c * b`.
|
Int.add_one_le_of_lt
theorem Int.add_one_le_of_lt : ∀ {a b : ℤ}, a < b → a + 1 ≤ b
This theorem states that for any two integer variables, `a` and `b`, if `a` is less than `b`, then the sum of `a` and 1 is less than or equal to `b`. In mathematical terms, if \(a < b\), then \(a + 1 \leq b\).
More concisely: For all integers a and b, if a < b then a + 1 <= b.
|
Int.neg_lt_neg
theorem Int.neg_lt_neg : ∀ {a b : ℤ}, a < b → -b < -a
This theorem states that for any two integers `a` and `b`, if `a` is less than `b`, then the negation of `b` is less than the negation of `a`. That is, flipping the signs of two integers reverses their order.
More concisely: If `a` < `b`, then `-b` < `-a`. (Negating the two integers reverses their order.)
|
Int.add_lt_add_right
theorem Int.add_lt_add_right : ∀ {a b : ℤ}, a < b → ∀ (c : ℤ), a + c < b + c
This theorem states that for any two integers `a` and `b`, if `a` is less than `b`, then for any integer `c`, the sum of `a` and `c` is less than the sum of `b` and `c`. In other words, adding the same integer to both `a` and `b` maintains the original inequality between `a` and `b`. This is a property of the integers under addition and is a fundamental characteristic of the order structure on the integers.
More concisely: For all integers a, b, and c, if a < b then a + c < b + c.
|
Int.sub_nonneg_of_le
theorem Int.sub_nonneg_of_le : ∀ {a b : ℤ}, b ≤ a → 0 ≤ a - b
This theorem, `Int.sub_nonneg_of_le`, states that for any two integers `a` and `b`, if `b` is less than or equal to `a` (denoted by `b ≤ a`), then the result of the subtraction of `b` from `a` (denoted by `a - b`) is guaranteed to be non-negative (denoted by `0 ≤ a - b`). In other words, it asserts that in the integer domain, subtracting a smaller number or an equal number from a larger or equal number always results in a non-negative number.
More concisely: For all integers a and b, if b ≤ a then 0 ≤ a - b.
|
Int.ofNat_lt
theorem Int.ofNat_lt : ∀ {n m : ℕ}, ↑n < ↑m ↔ n < m
This theorem states that for any two natural numbers `n` and `m`, the statement "the integer representation of `n` is less than the integer representation of `m`" is equivalent to "n is less than m". Essentially, if `n` and `m` are natural numbers, then their order relation remains the same when they are converted to integers.
More concisely: For any natural numbers n and m, n < m if and only if the integer representation of n is less than the integer representation of m.
|
Int.natAbs_lt_natAbs_of_nonneg_of_lt
theorem Int.natAbs_lt_natAbs_of_nonneg_of_lt : ∀ {a b : ℤ}, 0 ≤ a → a < b → a.natAbs < b.natAbs
The theorem `Int.natAbs_lt_natAbs_of_nonneg_of_lt` states that for any two integers `a` and `b`, if `a` is nonnegative (i.e., `a` is greater than or equal to 0) and `a` is less than `b`, then the absolute value of `a` is less than the absolute value of `b`. Here the absolute value of an integer is defined by the function `Int.natAbs`, which is the non-negative equivalent of the integer.
More concisely: For any integers `a` and `b`, if `a` is non-negative and `a` is strictly less than `b`, then `|a| < |b|`, where `|.|` denotes the absolute value function.
|
Int.add_lt_add_of_le_of_lt
theorem Int.add_lt_add_of_le_of_lt : ∀ {a b c d : ℤ}, a ≤ b → c < d → a + c < b + d
This theorem states that for any four integers `a`, `b`, `c`, and `d`, if `a` is less than or equal to `b` and `c` is strictly less than `d`, then the sum of `a` and `c` is strictly less than the sum of `b` and `d`. In mathematical terms, it can be represented as: if \(a \leq b\) and \(c < d\), then \(a + c < b + d\).
More concisely: If `a` ≤ `b` and `c` < `d`, then `a + c` < `b + d`. (Or, in mathematical notation: a ≤ b ∧ c < d → a + c < b + d.)
|
Int.eq_succ_of_zero_lt
theorem Int.eq_succ_of_zero_lt : ∀ {a : ℤ}, 0 < a → ∃ n, a = ↑n.succ
This theorem declares that for any integer `a`, if `a` is greater than zero (0 < a), then there exists a natural number `n` such that `a` is equal to the successor of `n` (a = n + 1). In other words, any positive integer can be expressed as the successor of some natural number.
More concisely: For any positive integer `a`, there exists a natural number `n` such that `a = n + 1`.
|
Int.zero_lt_one
theorem Int.zero_lt_one : 0 < 1
This theorem, `Int.zero_lt_one`, states that zero is less than one in the set of integers. In other words, it asserts the fundamental ordering of numbers on the number line where 0 is to the left of 1, hence less than 1. This is a basic and universally accepted principle in number theory.
More concisely: The theorem `Int.zero_lt_one` asserts that 0 < 1 in the set of integers.
|
Int.le_trans
theorem Int.le_trans : ∀ {a b c : ℤ}, a ≤ b → b ≤ c → a ≤ c
This theorem, `Int.le_trans`, states the transitive property of less than or equal to relation for integers. Specifically, for any three integers `a`, `b`, and `c`, if `a` is less than or equal to `b` and `b` is less than or equal to `c`, then it follows that `a` is less than or equal to `c`.
More concisely: If `a ≤ b` and `b ≤ c`, then `a ≤ c`. (In other words, the transitive property holds for the integer less-than-or-equal-to relation.)
|
Int.add_le_add_left
theorem Int.add_le_add_left : ∀ {a b : ℤ}, a ≤ b → ∀ (c : ℤ), c + a ≤ c + b
This theorem states that for any integers `a`, `b`, and `c`, if `a` is less than or equal to `b`, then the result of adding `c` to `a` is less than or equal to the result of adding `c` to `b`. Essentially, it means that adding the same integer to both sides of a less than or equal to comparison doesn't change the truth of the inequality in the domain of integers.
More concisely: For all integers `a`, `b`, and `c`, if `a ≤ b`, then `a + c ≤ b + c`.
|
Int.lt_iff_le_not_le
theorem Int.lt_iff_le_not_le : ∀ {a b : ℤ}, a < b ↔ a ≤ b ∧ ¬b ≤ a
This theorem states that for any two integers `a` and `b`, `a` is less than `b` if and only if `a` is less than or equal to `b` and it is not true that `b` is less than or equal to `a`. Essentially, it confirms that `a` is strictly less than `b` only when `a` is at most `b` and `b` is not at most `a`.
More concisely: For integers `a` and `b`, `a` is strictly less than `b` if and only if `a` is less than `b` and `b` is not less than `a`.
|
Int.eq_nat_or_neg
theorem Int.eq_nat_or_neg : ∀ (a : ℤ), ∃ n, a = ↑n ∨ a = -↑n
This theorem states that for every integer `a`, there exists a natural number `n` such that `a` equals `n` or `a` equals negative `n`. In other words, any integer is either a natural number or the negative of a natural number. This theorem embodies the concept that integers are composed of natural numbers and their negatives.
More concisely: For every integer `a`, there exists a natural number `n` such that `a = n` or `a = -n`.
|
Int.add_lt_add_of_lt_of_le
theorem Int.add_lt_add_of_lt_of_le : ∀ {a b c d : ℤ}, a < b → c ≤ d → a + c < b + d
This theorem states that for all integers `a`, `b`, `c`, and `d`, if `a` is less than `b` and `c` is less than or equal to `d`, then the sum of `a` and `c` is less than the sum of `b` and `d`. This theorem is a fundamental result in order theory and is applicable to integers in this context.
More concisely: For all integers `a`, `b`, `c`, and `d`, if `a < b` and `c <= d`, then `a + c < b + d`.
|
Int.toNat_eq_max
theorem Int.toNat_eq_max : ∀ (a : ℤ), ↑a.toNat = max a 0
This theorem states that for any integer 'a', the natural number obtained by converting 'a' using the 'Int.toNat' function is equal to the larger value between 'a' and '0'. In other words, for any integer, the natural number version of it is its maximum with zero. If 'a' is a positive integer or zero, the 'Int.toNat' function will give 'a' itself. But if 'a' is negative, the 'Int.toNat' function will give '0', which is the maximum of 'a' and '0'.
More concisely: For any integer 'a', the natural number obtained by converting 'a' using the 'Int.toNat' function is the maximum of 'a' and '0'.
|
Int.add_le_add
theorem Int.add_le_add : ∀ {a b c d : ℤ}, a ≤ b → c ≤ d → a + c ≤ b + d
This theorem states that for any four integers `a`, `b`, `c`, `d`, if `a` is less than or equal to `b` and `c` is less than or equal to `d`, then the sum of `a` and `c` is also less than or equal to the sum of `b` and `d`. In other words, in the integer domain, the sum of two quantities will not exceed the sum of their upper bounds.
More concisely: For all integers a, b, c, and d, if a <= b and c <= d then a + c <= b + d.
|
Int.sign_eq_neg_one_of_neg
theorem Int.sign_eq_neg_one_of_neg : ∀ {a : ℤ}, a < 0 → a.sign = -1
The theorem `Int.sign_eq_neg_one_of_neg` states that for any integer `a`, if `a` is less than zero, then the sign of `a` is `-1`. This is expressed in terms of the `Int.sign` function, which assigns an integer "sign" to any given integer: `1` for positive numbers, `0` for zero, and `-1` for negative numbers. Thus, this theorem formalizes the intuitive understanding that the sign of a negative number is `-1`.
More concisely: For any integer `a`, if `a` is negative then `Int.sign a = -1`.
|
Int.natAbs_eq_iff
theorem Int.natAbs_eq_iff : ∀ {a : ℤ} {n : ℕ}, a.natAbs = n ↔ a = ↑n ∨ a = -↑n
The theorem `Int.natAbs_eq_iff` states that for any integer `a` and natural number `n`, the absolute value of `a` is equal to `n` if and only if `a` is equal to the integer representation of `n` (notated `↑n`) or `a` is equal to the negative of the integer representation of `n` (notated `-↑n`). In other words, this theorem relates the absolute value function on integers with positive and negative numbers: an integer's absolute value is some natural number if and only if the integer is either that number or its negation.
More concisely: The absolute value of an integer equals a natural number if and only if the integer is that number or its negative.
|
Int.mul_lt_mul_of_pos_left
theorem Int.mul_lt_mul_of_pos_left : ∀ {a b c : ℤ}, a < b → 0 < c → c * a < c * b
This theorem states that for any three integers `a`, `b`, and `c`, if `a` is less than `b` and `c` is positive, then the product of `c` and `a` is less than the product of `c` and `b`. In essence, it confirms that multiplication by a positive integer preserves the order of other integers.
More concisely: For any integers `a` < `b` and positive integer `c`, `c` * `a` < `c` * `b`.
|
Int.natAbs_ne_zero
theorem Int.natAbs_ne_zero : ∀ {a : ℤ}, a.natAbs ≠ 0 ↔ a ≠ 0
The theorem `Int.natAbs_ne_zero` states that for any integer `a`, the absolute value of `a` is not equal to zero if and only if `a` is not equal to zero. This is a bi-directional implication, which means that both the conditions imply each other. If the absolute value of an integer is not zero, then the integer itself is not zero, and conversely, if an integer is not zero, then its absolute value is also not zero.
More concisely: For any integer `a`, |a| ≠ 0 if and only if a ≠ 0.
|
Int.le_antisymm
theorem Int.le_antisymm : ∀ {a b : ℤ}, a ≤ b → b ≤ a → a = b
This theorem, `Int.le_antisymm`, states that for any two integers `a` and `b`, if `a` is less than or equal to `b` and `b` is also less than or equal to `a`, then `a` and `b` must be equal. This is basically the antisymmetry property of the less than or equal to (`≤`) relation on integers. In mathematical notation this can be written as: ∀a, b ∈ ℤ, if a ≤ b and b ≤ a then a = b.
More concisely: For all integers `a` and `b`, if `a` is less than or equal to `b` and `b` is less than or equal to `a`, then `a` equals `b`. (Or, symbolically: ∀a b ∈ ℤ, a ≤ b ∧ b ≤ a → a = b)
|
Int.lt_iff_add_one_le
theorem Int.lt_iff_add_one_le : ∀ (a b : ℤ), a < b ↔ a + 1 ≤ b
This theorem states that for any two integers `a` and `b`, `a` is less than `b` if and only if `a + 1` is less than or equal to `b`. This is a fundamental concept in the notion of ordering on the integers, reflecting that the next integer after `a` (`a+1`) is either equal to `b` or precedes `b`.
More concisely: For all integers a and b, a < b if and only if a + 1 <= b.
|
Int.le.dest
theorem Int.le.dest : ∀ {a b : ℤ}, a ≤ b → ∃ n, a + ↑n = b
This theorem, `Int.le.dest`, states that for any two integers `a` and `b`, if `a` is less than or equal to `b`, then there exists a non-negative integer `n` such that when `n` is added to `a`, we get `b`. In other words, it confirms the intuitive notion that `b` can be reached by adding some non-negative number to `a` when `a` is less than or equal to `b`.
More concisely: For any integers `a` and `b` with `a ≤ b`, there exists a non-negative integer `n` such that `a + n = b`.
|
Int.le_add_of_sub_right_le
theorem Int.le_add_of_sub_right_le : ∀ {a b c : ℤ}, a - c ≤ b → a ≤ b + c
This theorem, `Int.le_add_of_sub_right_le`, states that for any three integers `a`, `b`, and `c`, if `a - c` is less than or equal to `b`, then `a` is less than or equal to `b + c`. In mathematical terms, it's expressing the inequality relation: if `a - c ≤ b`, then it must be the case that `a ≤ b + c`.
More concisely: If `a - c` is less than or equal to `b`, then `a` is less than or equal to `b + c`. In mathematical notation, `a - c ≤ b` implies `a ≤ b + c`.
|
Int.le_of_lt_add_one
theorem Int.le_of_lt_add_one : ∀ {a b : ℤ}, a < b + 1 → a ≤ b
This theorem, `Int.le_of_lt_add_one`, states that for all integer values `a` and `b`, if `a` is less than `b + 1`, then `a` is also less than or equal to `b`. It establishes a relationship between the "less than" and "less than or equal to" comparisons in the context of integer arithmetic.
More concisely: For all integers `a` and `b`, if `a` is less than `b + 1`, then `a` is less than or equal to `b`.
|
Int.add_lt_add_left
theorem Int.add_lt_add_left : ∀ {a b : ℤ}, a < b → ∀ (c : ℤ), c + a < c + b
This theorem states that for all integers `a` and `b`, if `a` is less than `b`, then for any integer `c`, the sum of `c` and `a` is less than the sum of `c` and `b`. In mathematical terms, if $a < b$, then for all $c$, we have $c + a < c + b$. This is a formalization of the concept of preserving inequality under the addition of the same integer to both sides.
More concisely: For all integers `a` and `b` where `a` < `b`, the sum of any integer `c` with `a` is less than the sum of `c` with `b`. Mathematically, if $a < b$, then for all $c$, we have $c + a < c + b$.
|
Int.add_one_le_iff
theorem Int.add_one_le_iff : ∀ {a b : ℤ}, a + 1 ≤ b ↔ a < b
This theorem, `Int.add_one_le_iff`, is a law about integers in Lean 4. It states that for any two integers `a` and `b`, the statement "`a + 1` is less than or equal to `b`" is equivalent to the statement "`a` is less than `b`". In other words, adding one to `a` and checking if the result is less than or equal to `b` is the same as directly comparing `a` with `b` in terms of less than relation.
More concisely: For integers `a` and `b`, `a + 1 ≤ b` if and only if `a < b`.
|
Int.mul_le_mul_of_nonneg_right
theorem Int.mul_le_mul_of_nonneg_right : ∀ {a b c : ℤ}, a ≤ b → 0 ≤ c → a * c ≤ b * c
This theorem states that for any three integers `a`, `b`, and `c`, if `a` is less than or equal to `b` and `c` is non-negative (greater than or equal to zero), then the product of `a` and `c` is less than or equal to the product of `b` and `c`. Essentially, this theorem is capturing the idea that multiplication by a non-negative integer preserves the order of other integers.
More concisely: For integers `a` ≤ `b` and non-negative integer `c`, `a` * `c` ≤ `b` * `c`.
|
Int.natAbs_neg
theorem Int.natAbs_neg : ∀ (a : ℤ), (-a).natAbs = a.natAbs
This theorem states that for every integer `a`, the absolute value of the negation of `a` is equal to the absolute value of `a` itself. In other words, if you take the negative of an integer and compute its absolute value, you will get the same result as if you took the absolute value of the original integer. This is consistent with the mathematical concept that the absolute value of a number is always non-negative, regardless of whether the number itself is positive or negative.
More concisely: For all integers a, |-a| = |a|.
|
Int.ofNat_le
theorem Int.ofNat_le : ∀ {m n : ℕ}, ↑m ≤ ↑n ↔ m ≤ n
This theorem, `Int.ofNat_le`, states that for all natural numbers `m` and `n`, the statement "the integer representation of `m` is less than or equal to the integer representation of `n`" is equivalent to " `m` is less than or equal to `n`". In other words, it specifies the order preservation property under the natural number to integer mapping.
More concisely: The theorem `Int.ofNat_le` asserts that for all natural numbers `m` and `n`, `m ≤ n` if and only if `Int.ofNat m ≤ Int.ofNat n`.
|
Int.neg_le_neg
theorem Int.neg_le_neg : ∀ {a b : ℤ}, a ≤ b → -b ≤ -a
This theorem states that for all integers `a` and `b`, if `a` is less than or equal to `b`, then `-b` is less than or equal to `-a`. In other words, the negation of a larger integer is less than or equal to the negation of a smaller integer.
More concisely: For all integers `a` and `b`, if `a ≤ b`, then `-b ≤ -a`.
|
Int.lt_irrefl
theorem Int.lt_irrefl : ∀ (a : ℤ), ¬a < a
This theorem states that for any integer `a`, it is not possible for `a` to be less than itself. In other words, there are no integer values for which the proposition "this integer is less than itself" would be true. This is a fundamental rule in mathematics, often referred to as the irreflexivity of the 'less than' relationship for integers.
More concisely: For all integers a, a is not less than a.
|
Int.negSucc_lt_zero
theorem Int.negSucc_lt_zero : ∀ (n : ℕ), Int.negSucc n < 0
This theorem states that for any natural number `n`, the negative of the successor of `n` (represented as `Int.negSucc n` in Lean 4) is less than zero. In other words, if you take any natural number, increment it by one, and then take the negative of the result, the final result will always be a negative integer, i.e., less than zero.
More concisely: For any natural number `n`, `- (Suc n) < 0`, where `Suc` represents the successor function.
|
Int.mul_lt_mul_of_pos_right
theorem Int.mul_lt_mul_of_pos_right : ∀ {a b c : ℤ}, a < b → 0 < c → a * c < b * c
This theorem states that for all integers `a`, `b`, and `c`, if `a` is less than `b` and `c` is a positive number, then the product of `a` and `c` is less than the product of `b` and `c`. In other words, for positive integers `c`, multiplication by `c` preserves the order of other integers.
More concisely: If `a` < `b` are integers and `c` is a positive number, then `ac` < `bc`.
|
Int.lt_add_of_sub_left_lt
theorem Int.lt_add_of_sub_left_lt : ∀ {a b c : ℤ}, a - b < c → a < b + c
This theorem states that for any three integers `a`, `b`, and `c`, if the difference of `a` and `b` is less than `c`, then `a` is less than the sum of `b` and `c`. In mathematical terms, if `a - b < c` then `a < b + c`. This theorem is a basic property of integers and their operations.
More concisely: If `a`, `b`, and `c` are integers with `a - b < c`, then `a < b + c`.
|
Int.le_of_neg_le_neg
theorem Int.le_of_neg_le_neg : ∀ {a b : ℤ}, -b ≤ -a → a ≤ b
This theorem states that for any two integers `a` and `b`, if the negative of `b` is less than or equal to the negative of `a`, then `a` is less than or equal to `b`. This is a property of the order relation on the integers, and captures the idea that reversing the order of the integers also reverses the inequality.
More concisely: If `a` and `b` are integers, then `a <= b` if and only if `-b <= -a`.
|
Int.natAbs_add_le
theorem Int.natAbs_add_le : ∀ (a b : ℤ), (a + b).natAbs ≤ a.natAbs + b.natAbs
The theorem `Int.natAbs_add_le` states that for any two integers `a` and `b`, the absolute value of their sum is less than or equal to the sum of their absolute values. In other words, given any two integers, the absolute value of their sum doesn't exceed the sum of their individual absolute values. This is represented mathematically as `|a + b| ≤ |a| + |b|`, where `|x|` denotes the absolute value of `x`.
More concisely: The absolute value of the sum of two integers is less than or equal to the sum of their absolute values. | |a| + |b| ≤ |a + b|.
|
Int.natAbs_eq_natAbs_iff
theorem Int.natAbs_eq_natAbs_iff : ∀ {a b : ℤ}, a.natAbs = b.natAbs ↔ a = b ∨ a = -b
The theorem `Int.natAbs_eq_natAbs_iff` states that, for any two integers `a` and `b`, the absolute value of `a` is equal to the absolute value of `b` if and only if `a` is equal to `b` or `a` is equal to the negation of `b`. In other words, two integers have the same absolute value if they are either the same number or each other's opposites.
More concisely: For integers `a` and `b`, |a| = |b| if and only if a = b or a = -b.
|
Int.sign_zero
theorem Int.sign_zero : Int.sign 0 = 0
The theorem `Int.sign_zero` asserts that the sign of the integer 0 is also 0. In other words, when the function `Int.sign` is applied to the integer 0, it returns 0, which is consistent with the definition of the sign function that assigns `0` to `0`, `1` to positive integers, and `-1` to negative integers.
More concisely: The sign of integer 0 is 0. (or equivalently, Int.sign 0 = 0)
|
Int.le_total
theorem Int.le_total : ∀ (a b : ℤ), a ≤ b ∨ b ≤ a
This theorem, `Int.le_total`, states that for all integer pairs `(a, b)`, either `a` is less than or equal to `b`, or `b` is less than or equal to `a`. In other words, given any two integers, one is always less than or equal to the other. This is a formalized expression of the total order property of the integers.
More concisely: For all integers a and b, either a ≤ b or b ≤ a.
|
Int.sub_left_lt_of_lt_add
theorem Int.sub_left_lt_of_lt_add : ∀ {a b c : ℤ}, a < b + c → a - b < c
This theorem states that for any three integers `a`, `b`, and `c`, if `a` is less than the sum of `b` and `c` (`a < b + c`), then `a` minus `b` is less than `c` (`a - b < c`). This theorem can be used to move terms around inequalities involving integer addition and subtraction.
More concisely: If `a` is less than the sum of `b` and `c` (`a < b + c`), then `a - b` is less than `c` (`a - b < c`).
|
Int.lt.dest
theorem Int.lt.dest : ∀ {a b : ℤ}, a < b → ∃ n, a + ↑n.succ = b
The theorem `Int.lt.dest` states that for any two integers `a` and `b`, if `a` is less than `b`, then there exists a natural number `n` such that `a` plus the successor of `n` (i.e., `n+1`) equals `b`. Essentially, this theorem formalizes the idea that if one integer is less than another, there is a specific positive difference between them.
More concisely: For any integers `a` and `b` with `a < b`, there exists a natural number `n` such that `a + (Suc n) = b`.
|
Int.le.intro
theorem Int.le.intro : ∀ {a b : ℤ} (n : ℕ), a + ↑n = b → a ≤ b
This theorem, `Int.le.intro`, establishes that for any two integers `a` and `b`, and a natural number `n`, if `a` plus the conversion of `n` to an integer equals `b`, then `a` is less than or equal to `b`. Basically, it states that if you can add a natural number to `a` to get `b`, then `a` must be less than or equal to `b`.
More concisely: For all integers `a` and `b` and natural number `n`, if `a + (nat.to_int n) = b`, then `a ≤ b`.
|
Int.self_le_toNat
theorem Int.self_le_toNat : ∀ (a : ℤ), a ≤ ↑a.toNat
This theorem states that for any integer `a`, `a` is less than or equal to the natural number that `a` is converted to using the `Int.toNat` function. In terms of mathematical notation, for all integers `a`, `a` ≤ `Int.toNat(a)`. It is important to note that the `Int.toNat` function converts an integer into a natural number with negative numbers becoming `0`. Thus, for negative integers, the theorem verifies that they are always less than or equal to `0`.
More concisely: For all integers `a`, `a` is less than or equal to the natural number `Int.toNat(a)`.
|
Int.natAbs_mul
theorem Int.natAbs_mul : ∀ (a b : ℤ), (a * b).natAbs = a.natAbs * b.natAbs
The theorem `Int.natAbs_mul` states that for any two integers `a` and `b`, the absolute value of the product of `a` and `b` is equal to the product of the absolute values of `a` and `b`. In other words, in mathematical terms, it expresses that |ab| = |a|*|b| for all integers `a` and `b`. This theorem essentially shows that the function `Int.natAbs` (which converts an integer to its absolute value) is multiplicative.
More concisely: For all integers a and b, |ab| = |a| * |b|.
|
Int.ofNat_zero_le
theorem Int.ofNat_zero_le : ∀ (n : ℕ), 0 ≤ ↑n
This theorem, `Int.ofNat_zero_le`, states that for any natural number `n`, the value of `n` when converted (or 'lifted') to an integer is always greater than or equal to zero. This is a standard fact about natural numbers, as they are defined to start from zero and increase, so there are no negative values. The `↑n` notation is used in Lean to denote the act of 'lifting' or 'casting' a value from one type to another, in this case, from natural numbers (`ℕ`) to integers (`ℤ`).
More concisely: For any natural number `n`, the integer obtained by lifting `n` is non-negative, i.e., `↑n ≥ 0`.
|
Int.ne_of_gt
theorem Int.ne_of_gt : ∀ {a b : ℤ}, b < a → a ≠ b
This theorem states that for any two integers `a` and `b`, if `b` is less than `a`, then `a` is not equal to `b`. The `∀` symbol indicates that this rule applies for all possible integers `a` and `b`. The `→` symbol is an implication, meaning that `b < a` being true directly implies `a ≠ b` is also true.
More concisely: For all integers `a` and `b`, if `b` is less than `a`, then `a` is not equal to `b`. In mathematical notation: `∀ (a b: ℤ), b < a → a ≠ b`.
|
Int.sign_eq_one_of_pos
theorem Int.sign_eq_one_of_pos : ∀ {a : ℤ}, 0 < a → a.sign = 1
This theorem states that for any integer 'a', if 'a' is greater than 0, then the sign of 'a' is 1. This is essentially saying that the "sign" function, which returns the "sign" of an integer as another integer, will return 1 for all positive integers.
More concisely: For all integers 'a', if 'a' > 0 then sign 'a' = 1.
|
Int.natAbs_ofNat
theorem Int.natAbs_ofNat : ∀ (n : ℕ), (↑n).natAbs = n
The theorem `Int.natAbs_ofNat` states that for every natural number `n`, the absolute value of the integer representation of `n` is `n` itself. In other words, when a natural number is considered as an integer and its absolute value is taken, it remains the same. This is because natural numbers are non-negative and so their absolute value doesn't change. In mathematical notation, the theorem is saying that for all natural numbers `n`, |n| = n.
More concisely: The theorem `Int.natAbs_ofNat` asserts that for all natural numbers `n`, the absolute value of their integer representation equals `n` itself.
|
Int.lt_or_gt_of_ne
theorem Int.lt_or_gt_of_ne : ∀ {a b : ℤ}, a ≠ b → a < b ∨ b < a
This theorem states that for any two integer numbers `a` and `b`, if `a` is not equal to `b`, then `a` is either less than `b` or `b` is less than `a`. In other words, if two integers are not equal, one must be less than the other.
More concisely: For all integers a and b, if a ≠ b then a < b or b < a.
|
Int.ofNat_nonneg
theorem Int.ofNat_nonneg : ∀ (n : ℕ), 0 ≤ ↑n
This theorem, `Int.ofNat_nonneg`, states that for any natural number `n`, the integer representation of `n` is always non-negative. In mathematical terms, given any natural number `n`, the inequality `0 ≤ n` holds when `n` is considered as an integer.
More concisely: For any natural number `n`, `0 ≤ Int.ofNat n`.
|
Int.lt_add_of_sub_right_lt
theorem Int.lt_add_of_sub_right_lt : ∀ {a b c : ℤ}, a - c < b → a < b + c
This theorem states that for any three integers `a`, `b`, and `c`, if the difference of `a` and `c` is less than `b`, then `a` is less than the sum of `b` and `c`. In other words, for all integers `a`, `b`, `c`, if `a - c < b`, it follows that `a < b + c`. This is a piece of order theory in the domain of integers.
More concisely: If `a`, `b`, and `c` are integers with `a - c < b`, then `a < b + c`.
|
Int.natAbs_mul_self
theorem Int.natAbs_mul_self : ∀ {a : ℤ}, ↑(a.natAbs * a.natAbs) = a * a
This theorem states that for any integer `a`, the square of the absolute value of `a` (denoted `(Int.natAbs a * Int.natAbs a)`) is equivalent to the square of `a` itself (denoted `a * a`). In other words, it says that the absolute value function (when applied to an integer and then squared) doesn't change the result of squaring the original integer.
More concisely: For any integer `a`, the square of its absolute value is equal to the square of `a` itself: `(Int.natAbs a) ^ 2 = a ^ 2`.
|