lt_or_gt_of_ne
theorem lt_or_gt_of_ne : ∀ {α : Type u} [inst : LinearOrder α] {a b : α}, a ≠ b → a < b ∨ a > b
This theorem, `lt_or_gt_of_ne`, states that for any given type `α` that has a linear order, for any two elements `a` and `b` of that type, if `a` is not equal to `b`, then either `a` is less than `b` or `a` is greater than `b`. In other words, in any ordered set, any two distinct elements can be compared in such a way that one is strictly less or strictly greater than the other.
More concisely: For any type `α` with a linear order, if `a` and `b` are distinct elements of `α`, then `a < b` or `b < a`.
|
Decidable.lt_or_eq_of_le
theorem Decidable.lt_or_eq_of_le :
∀ {α : Type u} [inst : PartialOrder α] [inst_1 : DecidableRel fun x x_1 => x ≤ x_1] {a b : α},
a ≤ b → a < b ∨ a = b
This theorem, "Decidable.lt_or_eq_of_le", states that for any type `α` that has a partial order and a decidable relation on the less than or equal to (`≤`) operation, given two elements `a` and `b` from `α`, if `a` is less than or equal to `b`, then `a` is either strictly less than `b` or `a` is equal to `b`. Thus, it provides a mechanism to decide between the two possible outcomes of the less than or equal to (`≤`) comparison.
More concisely: For any type `α` with a decidable partial order `≤`, if `a ≤ b` then `a = b` or `a < b`.
|
le_or_lt
theorem le_or_lt : ∀ {α : Type u} [inst : LinearOrder α] (a b : α), a ≤ b ∨ b < a
This theorem, `le_or_lt`, states that for any type `α` that has a linear order, given two elements `a` and `b` of this type, it is always the case that either `a` is less than or equal to `b` or `b` is less than `a`. In other words, in any linear order, any two elements are either in their natural order or reverse order; there is no third option.
More concisely: For any linear ordered type `α`, for all `a` and `b` in `α`, either `a ≤ b` or `b < a`.
|
lt_or_le
theorem lt_or_le : ∀ {α : Type u} [inst : LinearOrder α] (a b : α), a < b ∨ b ≤ a
This theorem states that for any given type `α` that has a linear order, for all instances of `α` named `a` and `b`, either `a` is less than `b` or `b` is less than or equal to `a`. This is a fundamental principle of ordered sets, reflecting that any two elements can be compared, with one being less than (or possibly equal to, in case of non-strict ordering) the other.
More concisely: For any type `α` with a linear order, for all `a` and `b` of type `α`, either `a` is less than `b` or `b` is less than or equal to `a`.
|
lt_of_le_not_le
theorem lt_of_le_not_le : ∀ {α : Type u} [inst : Preorder α] {a b : α}, a ≤ b → ¬b ≤ a → a < b
This theorem, `lt_of_le_not_le`, states that for any type `α` with a preorder structure, given any two elements `a` and `b` of type `α`, if `a` is less than or equal to `b` and it is not the case that `b` is less than or equal to `a`, then `a` is strictly less than `b`. In other words, if `a` is not greater than or equal to `b` but is still not greater than `b`, then `a` must be less than `b`. This theorem provides a way of concluding strict inequality in a preordered set given partial order information.
More concisely: If `a` is related to `b` by a preorder and not reversely related, then `a` is strictly smaller than `b`.
|
le_of_not_ge
theorem le_of_not_ge : ∀ {α : Type u} [inst : LinearOrder α] {a b : α}, ¬a ≥ b → a ≤ b
This theorem, `le_of_not_ge`, states that for any type `α` having a linear order and for any two elements `a` and `b` of this type, if `a` is not greater than or equal to `b`, then `a` must be less than or equal to `b`. This is a fundamental property in ordered sets.
More concisely: If `α` is a type with a linear order and `a` is not greater than or equal to `b` in `α`, then `a` is less than or equal to `b`.
|
le_of_not_lt
theorem le_of_not_lt : ∀ {α : Type u} [inst : LinearOrder α] {a b : α}, ¬b < a → a ≤ b
This theorem, `le_of_not_lt`, states that for all types `α` that have a linear order, if it is not the case that `b` is less than `a`, then `a` is less than or equal to `b`. In other words, if `b` is not strictly lesser than `a` in a linearly ordered set, it must be that `a` is either equal to `b` or less than `b`.
More concisely: If `α` is a linearly ordered type and `a` is not less than `b` in `α`, then `a` is less than or equal to `b`.
|
not_lt
theorem not_lt : ∀ {α : Type u} [inst : LinearOrder α] {a b : α}, ¬a < b ↔ b ≤ a
This theorem, `not_lt`, states that for all types `α` that have a linear order, for any two elements `a` and `b` from this type, `a` is not less than `b` if and only if `b` is less than or equal to `a`. In other words, this theorem defines the relationship between the "not less than" and "less than or equal to" comparison operations in any ordered set.
More concisely: For all types with a linear order, `a` is not less than `b` if and only if `b` is less than or equal to `a`.
|
not_lt_of_ge
theorem not_lt_of_ge : ∀ {α : Type u} [inst : Preorder α] {a b : α}, a ≥ b → ¬a < b
This theorem, `not_lt_of_ge`, states that for any type `α` that has a preorder relationship defined on its elements, if `a` and `b` are two elements of this type and `a` is greater than or equal to `b`, then it is not possible that `a` is less than `b`. In simpler terms, this theorem asserts that in a preorder, no element can be simultaneously greater than or equal to and less than another element.
More concisely: In a preorder, for all types `α` and elements `a` and `b` of type `α`, if `a ≥ b`, then it is not the case that `a < b`.
|
le_not_le_of_lt
theorem le_not_le_of_lt : ∀ {α : Type u} [inst : Preorder α] {a b : α}, a < b → a ≤ b ∧ ¬b ≤ a
This theorem, `le_not_le_of_lt`, states that for any type `α` that has a preorder structure (denoted by `[inst : Preorder α]`), for any two elements `a` and `b` of this type, if `a` is strictly less than `b` (i.e., `a < b`), then two conditions hold: 1) `a` is less than or equal to `b` (i.e., `a ≤ b`), and 2) it is not the case that `b` is less than or equal to `a` (i.e., `¬b ≤ a`). In other words, the theorem ensures that the strict less than relation (`<`) implies the less than or equal to relation (`≤`), but not the other way around.
More concisely: If `α` is a preordered type and `a < b`, then `a ≤ b` and `¬b ≤ a`.
|
lt_of_le_of_lt
theorem lt_of_le_of_lt : ∀ {α : Type u} [inst : Preorder α] {a b c : α}, a ≤ b → b < c → a < c
This theorem states that for any type `α` that has a Preorder structure, if `a`, `b`, and `c` are elements of `α`, then if `a` is less than or equal to `b`, and `b` is strictly less than `c`, it follows that `a` is strictly less than `c`. In other words, if `a` is not greater than `b`, and `b` is less than `c`, then `a` is less than `c`. This is a fundamental property of ordered sets or fields.
More concisely: If `α` is a preordered type with `a ≤ b` and `b < c`, then `a < c`.
|
LinearOrder.max_def
theorem LinearOrder.max_def : ∀ {α : Type u} [self : LinearOrder α] (a b : α), max a b = if a ≤ b then b else a := by
sorry
The theorem `LinearOrder.max_def` states that for any type `α` that has a linear ordering, the function `max` which determines the maximum of two elements `a` and `b` is defined by a conditional statement: if `a` is less than or equal to `b`, then `b` is the maximum; otherwise, `a` is the maximum.
More concisely: For any type `α` with a linear ordering, the function `max` is defined as `if a <= b then b else a`.
|
lt_of_lt_of_le
theorem lt_of_lt_of_le : ∀ {α : Type u} [inst : Preorder α] {a b c : α}, a < b → b ≤ c → a < c
This theorem, `lt_of_lt_of_le`, states that for any type `α` that has a preorder structure, given three elements `a`, `b`, and `c` of type `α`, if `a` is less than `b` and `b` is less than or equal to `c`, then `a` is less than `c`. In mathematical terms, this is just stating the transitivity of less-than relationship in a preordered set.
More concisely: If `a` is less than `b` and `b` is less than or equal to `c` in a preordered set `α`, then `a` is less than `c`.
|
LinearOrder.le_total
theorem LinearOrder.le_total : ∀ {α : Type u} [self : LinearOrder α] (a b : α), a ≤ b ∨ b ≤ a
This theorem states that for any type `α` that has a linear order, for any two elements `a` and `b` of type `α`, either `a` is less than or equal to `b`, or `b` is less than or equal to `a`. Essentially, it is asserting that a linear order is total, meaning every pair of elements is comparable.
More concisely: In a linear order, for all elements a and b, either a ≤ b or b ≤ a.
|
LinearOrder.min_def
theorem LinearOrder.min_def : ∀ {α : Type u} [self : LinearOrder α] (a b : α), min a b = if a ≤ b then a else b := by
sorry
This theorem states that for any type `α` that has a `LinearOrder` structure, the minimum function `min` between two variables `a` and `b` of type `α` is equivalent to a function that returns `a` if `a` is less than or equal to `b` and `b` otherwise. In other words, it formalizes the concept of the minimum value between two elements in a linearly ordered set.
More concisely: For any type `α` with a `LinearOrder` structure, `min a b` equals `if h : a ≤ b then a else b`.
|
ne_of_lt
theorem ne_of_lt : ∀ {α : Type u} [inst : Preorder α] {a b : α}, a < b → a ≠ b
This theorem states that for any type `α` with a preorder (a set equipped with a binary relation that is reflexive and transitive), if `a` and `b` are elements of `α` and `a` is less than `b`, then `a` is not equal to `b`. In mathematical terms, this theorem asserts that for all `a` and `b` in a preordered set, `a < b` implies `a ≠ b`.
More concisely: In a preordered set, if `a` is less than `b`, then `a` is strictly less than `b`, that is, `a < b` implies `a ≠ b`.
|
compare_gt_iff_gt
theorem compare_gt_iff_gt : ∀ {α : Type u} [inst : LinearOrder α] {a b : α}, compare a b = Ordering.gt ↔ a > b := by
sorry
This theorem states that for any type `α` that has a linear order, given two instances `a` and `b` of this type, the comparison function `compare` will return `Ordering.gt` if and only if `a` is strictly greater than `b`. In other words, it establishes a connection between the result of the `compare` function and the strict inequality relation in a linearly ordered type.
More concisely: For any linearly ordered type `α`, `compare a b = Ordering.gt` if and only if `a` is strictly greater than `b`.
|
not_lt_of_gt
theorem not_lt_of_gt : ∀ {α : Type u} [inst : LinearOrder α] {a b : α}, a > b → ¬a < b
This theorem states that for all types `α` that possess a linear order, if a specific element `a` of this type is greater than another element `b`, then `a` cannot be less than `b`. In other words, in any ordered set, if one element is strictly greater than another, it cannot also be less than that other element. This is a formalization of a fundamental property of ordered sets.
More concisely: In any ordered set, for all elements `a` and `b`, if `a` is strictly greater than `b` (`a > b`), then it is not the case that `b` is strictly greater than `a` (`b > a`).
|
le_rfl
theorem le_rfl : ∀ {α : Type u} [inst : Preorder α] {a : α}, a ≤ a
This theorem, `le_rfl`, asserts that for any given type `α` that has a preorder (a binary relation indicating that, for every pair of elements in the set, one of them is less than or equal to the other), every element `a` of this type is less than or equal to itself. This is a reflexive property of preorders, where every element is related to itself in the defined order.
More concisely: For any preordered type `α`, every element `a` in `α` is less than or equal to itself. (That is, `a ≤ a` holds in every preorder.)
|
le_imp_le_of_lt_imp_lt
theorem le_imp_le_of_lt_imp_lt :
∀ {α : Type u} {β : Type u_1} [inst : Preorder α] [inst_1 : LinearOrder β] {a b : α} {c d : β},
(d < c → b < a) → a ≤ b → c ≤ d
This theorem states that for any types `α` and `β` with a preorder on `α` and a linear order on `β`, and for any elements `a`, `b` of `α` and `c`, `d` of `β`, if it is true that `d < c` implies `b < a`, then if `a ≤ b` it must follow that `c ≤ d`. This theorem is a formalization of a certain property of ordered sets.
More concisely: If `α` is a preordered type, `β` is linearly ordered, `a ≤ b` in `α`, and `d < c` in `β`, then `c ≤ d`.
|
Mathlib.Init.Order.Defs._auxLemma.2
theorem Mathlib.Init.Order.Defs._auxLemma.2 : ∀ {α : Type u} [inst : LinearOrder α] {a b : α}, (¬a ≤ b) = (b < a) := by
sorry
This theorem, `Mathlib.Init.Order.Defs._auxLemma.2`, states that for every type `α` that has a linear order, for any two elements `a` and `b` of type `α`, the statement "it's not true that `a` is less than or equal to `b`" is equivalent to " `b` is strictly less than `a`". In other words, `a` not being less than or equal to `b` is the same as saying `b` is less than `a`. This theorem captures one of the fundamental properties of ordered sets.
More concisely: For any type `α` with a linear order, `a` not less than or equal to `b` is equivalent to `b` being strictly less than `a`.
|
lt_of_not_ge
theorem lt_of_not_ge : ∀ {α : Type u} [inst : LinearOrder α] {a b : α}, ¬a ≥ b → a < b
This theorem states that for all types `α` that have a linear order, if it is not the case that `a` is greater than or equal to `b` (`¬a ≥ b`), then `a` is strictly less than `b` (`a < b`). In other words, if `a` is not greater than or equal to `b`, the only other possibility in a linear order is that `a` is less than `b`.
More concisely: In a linear order, if `a` is not greater than or equal to `b` (`a < b ∨ ¬(a ≥ b)`), then `a` is strictly less than `b` (`a < b`).
|
le_of_eq
theorem le_of_eq : ∀ {α : Type u} [inst : Preorder α] {a b : α}, a = b → a ≤ b
This theorem, `le_of_eq`, states that for any type `α` that has a Preorder relation, given any two elements `a` and `b` of this type, if `a` is equal to `b`, then `a` is less than or equal to `b`. This theorem is quite intuitive as it's clear that any element is less than or equal to itself, but it's nonetheless important in establishing the basic properties of a Preorder relation in a type.
More concisely: For any type `α` with a Preorder relation, if `a` is equal to `b`, then `a ≤ b` (where `≤` denotes the Preorder relation).
|
lt_iff_le_not_le
theorem lt_iff_le_not_le : ∀ {α : Type u} [inst : Preorder α] {a b : α}, a < b ↔ a ≤ b ∧ ¬b ≤ a
This theorem, `lt_iff_le_not_le`, applies to any type `α` that has a preorder relation defined on it. It establishes an equivalence between two conditions for two elements `a` and `b` of this type: firstly, `a` being strictly less than `b` (`a < b`), and secondly, `a` being less than or equal to `b` (`a ≤ b`) but not the case that `b` is less than or equal to `a` (`¬b ≤ a`). In other words, it provides a characterization of "strict less than" in terms of "less than or equal to" and negation, in the context of preordered sets.
More concisely: For any preordered type `α`, `a < b` if and only if `a ≤ b` and not `b ≤ a`.
|
compare_eq_iff_eq
theorem compare_eq_iff_eq : ∀ {α : Type u} [inst : LinearOrder α] {a b : α}, compare a b = Ordering.eq ↔ a = b := by
sorry
This theorem, `compare_eq_iff_eq`, states that for all types `α` that have a linear order, the comparison of two variables `a` and `b` of type `α` will equal `Ordering.eq` if and only if `a` and `b` are equal. In other words, in a linear ordering, the `compare` function returns `Ordering.eq` precisely when the two input values are the same.
More concisely: For all types `α` with a linear order, `compare a b = Ordering.eq` if and only if `a = b`.
|
le_total
theorem le_total : ∀ {α : Type u} [inst : LinearOrder α] (a b : α), a ≤ b ∨ b ≤ a
The theorem `le_total` states that for any type `α` that has a linear order, for any two elements `a` and `b` of type `α`, either `a` is less than or equal to `b` or `b` is less than or equal to `a`. This property signifies total order, where any two elements are comparable.
More concisely: For any type `α` with a linear order, for all `a, b` in `α`, either `a ≤ b` or `b ≤ a`.
|
le_of_not_le
theorem le_of_not_le : ∀ {α : Type u} [inst : LinearOrder α] {a b : α}, ¬a ≤ b → b ≤ a
The theorem `le_of_not_le` states that for all types `α` such that `α` has a linear order, for any two elements `a` and `b` of `α`, if it is not the case that `a` is less than or equal to `b`, then `b` is less than or equal to `a`. This theorem is essentially stating the trichotomy property of the linear order, which means that for any two elements in a set, one and only one of the following is true: the first element is less than the second, the first element is equal to the second, or the first element is greater than the second.
More concisely: If `α` is a type with a linear order and `a` and `b` are elements of `α` with `a` not less than or equal to `b`, then `b` is less than or equal to `a`.
|
lt_of_le_of_ne
theorem lt_of_le_of_ne : ∀ {α : Type u} [inst : PartialOrder α] {a b : α}, a ≤ b → a ≠ b → a < b
This theorem, `lt_of_le_of_ne`, states that for any type `α` that has a partial order, if `a` and `b` are elements of `α` such that `a` is less than or equal to `b` and `a` is not equal to `b`, then `a` is strictly less than `b`. Here, `≤` and `<` denote the partial order and strict order respectively.
More concisely: If `α` is a type with a partial order, and `a` and `b` are elements of `α` with `a ≤ b` and `a ≠ b`, then `a < b`.
|
le_iff_lt_or_eq
theorem le_iff_lt_or_eq : ∀ {α : Type u} [inst : PartialOrder α] {a b : α}, a ≤ b ↔ a < b ∨ a = b
This theorem, `le_iff_lt_or_eq`, states that for any given type `α` that has a partial order, `a` is less than or equal to `b` if and only if `a` is strictly less than `b` or `a` equals `b`. Here, `a` and `b` are elements of the type `α`. This theorem connects the "less than or equal to" relation to the "strictly less than" relation and the "equality" relation in the context of a partial order.
More concisely: For any type `α` with a partial order, `a ≤ b` if and only if `a < b` or `a = b`.
|
Decidable.eq_or_lt_of_le
theorem Decidable.eq_or_lt_of_le :
∀ {α : Type u} [inst : PartialOrder α] [inst_1 : DecidableRel fun x x_1 => x ≤ x_1] {a b : α},
a ≤ b → a = b ∨ a < b
This theorem, `Decidable.eq_or_lt_of_le`, asserts that for any type `α` that has a partial order and a decidable relation for the "less than or equal to" (`≤`) operation, given two elements `a` and `b` of the type `α`, if `a` is less than or equal to `b`, then either `a` is equal to `b` or `a` is strictly less than `b`. The theorem essentially states the trichotomy property for ordered types with a decidability predicate, specifically for the case when one element is less than or equal to another.
More concisely: For any type `α` with a decidable partial order `≤`, if `a ≤ b` then `a = b` or `a < b`.
|
ne_of_gt
theorem ne_of_gt : ∀ {α : Type u} [inst : Preorder α] {a b : α}, b < a → a ≠ b
This theorem states that for any preordered type `α` and any two elements `a` and `b` of this type, if `b` is strictly less than `a`, then `a` is not equal to `b`. The preordered type could be any type that has a preorder relation defined on it, such as the integers, real numbers, or other types where there is a sense of "less than" or "greater than". This theorem essentially captures the intuitive idea that in a preordered set, if one element is greater than another, they cannot be the same element.
More concisely: In a preordered type, if one element is strictly less than another, then they are not equal.
|
lt_asymm
theorem lt_asymm : ∀ {α : Type u} [inst : Preorder α] {a b : α}, a < b → ¬b < a
This theorem, `lt_asymm`, states that for any given type `α` with a preorder relation, and any two elements `a` and `b` of that type, if `a` is less than `b` then `b` cannot be less than `a`. This property is known as asymmetry of the less-than relation and is one of the defining characteristics of a preorder. This theorem is applicable to any type that has a preorder, such as the integers, the reals, or any other ordered set.
More concisely: If `a` is less than `b` in a preorder, then it is not the case that `b` is less than `a`.
|
not_le_of_gt
theorem not_le_of_gt : ∀ {α : Type u} [inst : Preorder α] {a b : α}, a > b → ¬a ≤ b
This theorem, `not_le_of_gt`, states that for any preordered type `α` and any two elements `a` and `b` of that type, if `a` is greater than `b`, then it cannot be the case that `a` is less than or equal to `b`. In mathematical terms, it says that if `a > b` then it is not possible that `a ≤ b` for any `a` and `b` in a given preordered set.
More concisely: For any preordered type `α` and elements `a` and `b` in `α`, if `a > b` then `a ≤ b` is false.
|
le_of_not_gt
theorem le_of_not_gt : ∀ {α : Type u} [inst : LinearOrder α] {a b : α}, ¬a > b → a ≤ b
This theorem states that for all types `α` that have a `LinearOrder` instance, if a specific condition holds true where a given element `a` of type `α` is not greater than another element `b` of type `α`, it follows that `a` is less than or equal to `b`. In mathematical terms, this can be expressed as "for all `a` and `b` in a set with a linear order, if `a` is not greater than `b`, then `a` must be less than or equal to `b`".
More concisely: For all types `α` with a `LinearOrder` instance, if `a ≤ b` then `a ≤ b` holds. (In other words, the reflexive transitivity of the linear order relation holds.)
|
LinearOrder.compare_eq_compareOfLessAndEq
theorem LinearOrder.compare_eq_compareOfLessAndEq :
∀ {α : Type u} [self : LinearOrder α] (a b : α), compare a b = compareOfLessAndEq a b
The theorem `LinearOrder.compare_eq_compareOfLessAndEq` states that for any type `α` equipped with a `LinearOrder` structure (which implies a total order), the comparison function `compare` between any two elements `a` and `b` of `α` is equivalent to the comparison function `compareOfLessAndEq`. This `compareOfLessAndEq` function is constructed from the two decidable relations `<` and `=`. In other words, it confirms that the `compare` function, which returns an `Ordering` (either `lt`, `eq`, or `gt`), is consistent with the decidable less-than and equality relations on `α`.
More concisely: For any type `α` with a total order, the comparison function `compare` is equivalent to the function `compareOfLessAndEq` constructed from decidable relations `<` and `=`.
|
le_refl
theorem le_refl : ∀ {α : Type u} [inst : Preorder α] (a : α), a ≤ a
This theorem states that for any type `α` which has a Preorder relation, the 'less than or equal to' relation `≤` is reflexive. In other words, for any element `a` of type `α`, `a` is always less than or equal to itself. This is a fundamental property of preorders in mathematical order theory.
More concisely: For any preorder `≤` on type `α`, `a ≤ a` holds for all `a : α`.
|
lt_trans
theorem lt_trans : ∀ {α : Type u} [inst : Preorder α] {a b c : α}, a < b → b < c → a < c
This theorem, `lt_trans`, is a statement about transitivity in the setting of preorders. Given any type `α` that has a preorder structure, for any three elements `a`, `b`, and `c` of that type, if `a` is less than `b` and `b` is less than `c`, then it follows that `a` is less than `c`. This is essentially a formalization of the transitivity property of inequalities in mathematics.
More concisely: If `α` is a preordered type and `a ≤ b` and `b ≤ c`, then `a ≤ c`.
|
Mathlib.Init.Order.Defs._auxLemma.1
theorem Mathlib.Init.Order.Defs._auxLemma.1 : ∀ {α : Type u} [inst : LinearOrder α] {a b : α}, (¬a < b) = (b ≤ a) := by
sorry
This theorem states that for any type `α` that has a linear order, and for any two elements `a` and `b` of this type, the statement "not `a` is less than `b`" is equivalent to the statement "`b` is less than or equal to `a`". In mathematical notation, this can be written as ¬(a < b) ↔ (b ≤ a). This is a fundamental property of linearly ordered sets.
More concisely: The negation of the linear order relation between two elements is equivalent to the reverse order relation in a linearly ordered type. (or) In a linearly ordered type, `a` and `b` are not ordered `<` if and only if `b` is ordered `≤` or `a`.
|
lt_irrefl
theorem lt_irrefl : ∀ {α : Type u} [inst : Preorder α] (a : α), ¬a < a
This theorem, named `lt_irrefl`, states that for any type `α` that has a preorder (a relation that is reflexive and transitive), an element of that type cannot be strictly less than itself. In other words, it is impossible for `a` to be less than `a` in any preordered set. This is a fundamental property of orderings in mathematics, often referred to as irreflexivity.
More concisely: In any preordered type, no element is strictly less than itself.
|
le_trans
theorem le_trans : ∀ {α : Type u} [inst : Preorder α] {a b c : α}, a ≤ b → b ≤ c → a ≤ c
This theorem states that, in any preorder, the less than or equal to (`≤`) relation is transitive. Specifically, for any type `α` with a preorder structure, and for any elements `a`, `b`, and `c` of `α`, if `a` is less than or equal to `b` and `b` is less than or equal to `c`, then `a` is less than or equal to `c`. Transitivity is a fundamental property of preorders and partial orders, and this theorem formalizes that characteristic in the context of the less than or equal to relation.
More concisely: In any preorder, if `a ≤ b` and `b ≤ c`, then `a ≤ c`.
|
lt_or_ge
theorem lt_or_ge : ∀ {α : Type u} [inst : LinearOrder α] (a b : α), a < b ∨ a ≥ b
This theorem, `lt_or_ge`, states that for any given type `α` that has a linear order, for any two elements `a` and `b` of type `α`, `a` is either less than `b` or `a` is greater than or equal to `b`. This is a fundamental property of linearly ordered sets, expressing that any two elements in such a set can be compared, and either one is less than the other or they are equal or the first one is greater.
More concisely: For all linearly ordered types `α` and elements `a` and `b` of type `α`, either `a < b` or `a >= b`.
|
ge_trans
theorem ge_trans : ∀ {α : Type u} [inst : Preorder α] {a b c : α}, a ≥ b → b ≥ c → a ≥ c
This theorem, `ge_trans`, states a fundamental property of preordered types in mathematics: the transitivity of the 'greater than or equal to' relation. Specifically, for any preordered type `α` and any three elements `a`, `b`, and `c` of this type, if `a` is greater than or equal to `b` and `b` is greater than or equal to `c`, then it follows that `a` is greater than or equal to `c`. This is an example of the transitive property in action, which is often used in mathematical reasoning and proofs.
More concisely: If `a >= b` and `b >= c` in a preordered type `α`, then `a >= c`.
|
le_of_lt
theorem le_of_lt : ∀ {α : Type u} [inst : Preorder α] {a b : α}, a < b → a ≤ b
This theorem, `le_of_lt`, states that for any type `α` that has a preorder structure, if one element `a` is strictly less than another element `b`, then `a` is also less than or equal to `b`. In other words, in a preordered set, the strict less-than relation implies the less-than-or-equal-to relation.
More concisely: For any preordered type `α`, if `a` is strictly less than `b`, then `a ≤ b`.
|
not_le
theorem not_le : ∀ {α : Type u} [inst : LinearOrder α] {a b : α}, ¬a ≤ b ↔ b < a
This theorem states that for any linearly ordered type `α` and any two elements `a` and `b` of this type, `a` is not less than or equal to `b` if and only if `b` is less than `a`. In other words, in a linear order, the assertion that `a` is not less than or equal to `b` is equivalent to asserting that `b` is strictly less than `a`.
More concisely: In a linearly ordered type, `a` is not less than or equal to `b` if and only if `b` is strictly less than `a`.
|
ne_iff_lt_or_gt
theorem ne_iff_lt_or_gt : ∀ {α : Type u} [inst : LinearOrder α] {a b : α}, a ≠ b ↔ a < b ∨ a > b
This theorem, `ne_iff_lt_or_gt`, states that for any type `α` equipped with a linear order, and for any two elements `a` and `b` of type `α`, the proposition "`a` is not equal to `b`" is equivalent to the proposition "`a` is less than `b` or `a` is greater than `b`". This theorem encapsulates one of the fundamental properties of linearly ordered sets, where two distinct elements must stand in a strict order relation.
More concisely: For any linearly ordered type `α` and elements `a` and `b` of `α`, `a ≠ b` if and only if `a` is strictly less than `b` or `a` is strictly greater than `b`.
|
le_antisymm
theorem le_antisymm : ∀ {α : Type u} [inst : PartialOrder α] {a b : α}, a ≤ b → b ≤ a → a = b
This theorem states that in a partially ordered set of type `α`, for any two elements `a` and `b` of this set, if `a` is less than or equal to `b` and `b` is less than or equal to `a`, then `a` must be equal to `b`. This property is known as antisymmetry and is one of the defining characteristics of a partial order.
More concisely: In a partially ordered set, if `a` is less than or equal to `b` and `b` is less than or equal to `a`, then `a` equals `b` (antisymmetry property).
|
lt_or_eq_of_le
theorem lt_or_eq_of_le : ∀ {α : Type u} [inst : PartialOrder α] {a b : α}, a ≤ b → a < b ∨ a = b
This theorem states that in a partial order for any given type, for any two elements `a` and `b` of that type, if `a` is less than or equal to `b`, then either `a` is strictly less than `b` or `a` is equal to `b`. A partial order is a binary relation that is reflexive, antisymmetric, and transitive, which are common properties in many mathematical structures.
More concisely: In a partial order, if `a` is less than or equal to `b`, then `a` is strictly less than `b` or `a` equals `b`.
|
le_or_gt
theorem le_or_gt : ∀ {α : Type u} [inst : LinearOrder α] (a b : α), a ≤ b ∨ a > b
This theorem, `le_or_gt`, states that for all types `α` that have a linear ordering (`LinearOrder`), for any two elements `a` and `b` of that type, either `a` is less than or equal to `b` (`a ≤ b`) or `a` is greater than `b` (`a > b`). In other words, for any given pair of elements in a linearly ordered set, one of them is always either less than or equal to, or greater than the other.
More concisely: For all linearly ordered types `α` and elements `a` and `b` of type `α`, either `a ≤ b` or `a > b`.
|
le_antisymm_iff
theorem le_antisymm_iff : ∀ {α : Type u} [inst : PartialOrder α] {a b : α}, a = b ↔ a ≤ b ∧ b ≤ a
This theorem, `le_antisymm_iff`, states that for any partially ordered type `α` and any two elements `a` and `b` of that type, `a` is equal to `b` if and only if `a` is less than or equal to `b` and `b` is less than or equal to `a`. This is a formalization of the antisymmetry property of partial orders.
More concisely: In a partially ordered type, two elements are equal if and only if they are both less than or equal to each other.
|
lt_iff_not_ge
theorem lt_iff_not_ge : ∀ {α : Type u} [inst : LinearOrder α] (x y : α), x < y ↔ ¬x ≥ y
The theorem `lt_iff_not_ge` states that for any type `α` with a linear order, for any two elements `x` and `y` from this type, `x` is less than `y` if and only if it is not the case that `x` is greater than or equal to `y`. In other words, it formalizes the intuitive notion that if `x` is not greater than or equal to `y`, then it must be less than `y`, and vice versa.
More concisely: For any type with a linear order, x is less than y if and only if it is not the case that x is greater than or equal to y. (Or equivalently, x < y if and only if x >= y does not hold.)
|
lt_trichotomy
theorem lt_trichotomy : ∀ {α : Type u} [inst : LinearOrder α] (a b : α), a < b ∨ a = b ∨ b < a
This theorem, named `lt_trichotomy`, describes a basic property of linearly ordered types in Lean 4. Given any two elements `a` and `b` of a type `α` that is linearly ordered (as specified by the `LinearOrder α` typeclass), one and only one of the following holds: `a` is less than `b`, `a` is equal to `b`, or `b` is less than `a`. This property is a key part of the definition of a linear (or total) order, and is a form of the law of trichotomy for ordered sets.
More concisely: For all linearly ordered types `α` and elements `a` and `b` in `α`, exactly one of `a < b`, `a = b`, or `b < a` holds.
|
compare_lt_iff_lt
theorem compare_lt_iff_lt : ∀ {α : Type u} [inst : LinearOrder α] {a b : α}, compare a b = Ordering.lt ↔ a < b := by
sorry
This theorem, named `compare_lt_iff_lt`, states that for all types `α` that have a `LinearOrder` instance, and for all `a` and `b` of type `α`, the function `compare` returns `Ordering.lt` if and only if `a` is less than `b`. In other words, it establishes the exact condition under which the `compare` function would return `Ordering.lt` in a linear order.
More concisely: For any type `α` with a `LinearOrder` instance, `compare a b` equals `Ordering.lt` if and only if `a` is strictly less than `b`.
|