Linarith.lt_irrefl
theorem Linarith.lt_irrefl : ∀ {α : Type u} [inst : Preorder α] {a : α}, ¬a < a
This theorem, `Linarith.lt_irrefl`, states that for any type `α` that is a preorder, for any element `a` of type `α`, it is not possible for `a` to be less than `a`. In other words, the "<" relation is irreflexive in a preorder: no element is less than itself.
More concisely: In any preorder type `α`, for all `a` in `α`, it holds that `a` is not less than `a`.
|
lt_zero_of_zero_gt
theorem lt_zero_of_zero_gt : ∀ {α : Type u_1} [inst : Zero α] [inst_1 : LT α] {a : α}, 0 > a → a < 0
This theorem, `lt_zero_of_zero_gt`, states that for any type `α` with a defined zero and less than (`LT`) relation, if zero is greater than a given element `a` of type `α` (expressed as `0 > a`), then `a` is less than zero (`a < 0`). Essentially, it asserts the reflexivity of the 'greater than' and 'less than' relationship around zero for any suitable type.
More concisely: For any type `α` with a defined zero and less than relation, if `0 > a`, then `a < 0`.
|
Linarith.eq_of_not_lt_of_not_gt
theorem Linarith.eq_of_not_lt_of_not_gt : ∀ {α : Type u_1} [inst : LinearOrder α] (a b : α), ¬a < b → ¬b < a → a = b
This theorem, `Linarith.eq_of_not_lt_of_not_gt`, states that for any type `α` that has a linear ordering, given any two elements `a` and `b` of type `α`, if `a` is not less than `b` and `b` is not less than `a`, then `a` must be equal to `b`. This is a basic property of total orderings, where two elements are either equal or one is less than the other.
More concisely: If `α` is a linedarly ordered type and `a` and `b` are elements of `α` with `a >= b` and `b >= a`, then `a = b`.
|
Linarith.mul_nonpos
theorem Linarith.mul_nonpos : ∀ {α : Type u_1} [inst : OrderedRing α] {a b : α}, a ≤ 0 → 0 < b → b * a ≤ 0
This theorem states that for any ordered ring `α`, for any two elements `a` and `b` in `α`, if `a` is less than or equal to zero and `b` is greater than zero, then the product of `b` and `a` is less than or equal to zero. Here, an ordered ring is a ring with an order relation that is compatible with the ring operations.
More concisely: In an ordered ring, the product of any element less than or equal to zero with any positive element is less than or equal to zero.
|
le_zero_of_zero_ge
theorem le_zero_of_zero_ge : ∀ {α : Type u_1} [inst : Zero α] [inst_1 : LE α] {a : α}, 0 ≥ a → a ≤ 0
This theorem, `le_zero_of_zero_ge`, states that for any type `α` which has a zero and an order relation (denoted by `LE`), if zero is greater than or equal to a number `a` of type `α` (expressed as `0 ≥ a`), then it follows that `a` must be less than or equal to zero (expressed as `a ≤ 0`). Essentially, it's a way of enforcing that if `0` is not less than `a`, then `a` must not be more than `0`, considering the properties of the ordering on the type `α`.
More concisely: If `α` is a type with a zero and `LE` order relation, then `0 ≥ a` implies `a ≤ 0`.
|
Linarith.mul_neg
theorem Linarith.mul_neg : ∀ {α : Type u_1} [inst : StrictOrderedRing α] {a b : α}, a < 0 → 0 < b → b * a < 0 := by
sorry
This theorem, `Linarith.mul_neg`, states that for any strict ordered ring `α`, if we have two elements `a` and `b` of this ring, if `a` is less than zero and `b` is greater than zero, then the product of `b` and `a` is less than zero. Here, a strict ordered ring is a ring that also has a total order compatible with the ring operations (addition and multiplication).
More concisely: In a strict ordered ring, the product of two elements with one being negative and the other positive is negative.
|
Linarith.lt_of_lt_of_eq
theorem Linarith.lt_of_lt_of_eq : ∀ {α : Type u_1} [inst : OrderedSemiring α] {a b : α}, a < 0 → b = 0 → a + b < 0 := by
sorry
This theorem states that, for any ordered semiring `α` and any elements `a` and `b` in `α`, if `a` is less than zero and `b` is equal to zero, then the sum of `a` and `b` is less than zero. In other words, in an ordered semiring, adding zero to a negative number results in a negative number.
More concisely: In an ordered semiring, the sum of a negative number and zero is still a negative number.
|