not_isMax
theorem not_isMax : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : NoMaxOrder α] (a : α), ¬IsMax a
The theorem `not_isMax` asserts that for any type `α` which has a preorder structure and also satisfies the `NoMaxOrder` condition (i.e., there is no maximal element in the set), any element `a` of type `α` cannot be a maximal element. In other words, in a set with a preorder structure without a maximum element, there always exists some other element that is strictly greater than any given element.
More concisely: In a preordered type without a maximum element, no element is maximal.
|
NoTopOrder.exists_not_le
theorem NoTopOrder.exists_not_le : ∀ {α : Type u_3} [inst : LE α] [self : NoTopOrder α] (a : α), ∃ b, ¬b ≤ a
This theorem states that for any type `α` which has an order (`LE α`) and is also a 'NoTopOrder' (i.e., it doesn't have a largest element), for any element `a` of type `α`, there exists another element `b` such that `b` is either not comparable to `a` or `b` is strictly larger than `a`. This is essentially saying that there is no 'largest' element in such ordered structures and for any given element, there's always another element which is not less than or equal to the given element.
More concisely: In any ordered type `α` without a top element, for every element `a`, there exists an element `b` such that `a` and `b` are not comparable or `b` is strictly greater than `a`.
|
NoBotOrder.exists_not_ge
theorem NoBotOrder.exists_not_ge : ∀ {α : Type u_3} [inst : LE α] [self : NoBotOrder α] (a : α), ∃ b, ¬a ≤ b
This theorem states that for any type `α` that has a less-than-or-equal-to operation (`LE α`) and does not have a least element (`NoBotOrder α`), for any given element `a` of type `α`, there exists another element `b` such that `a` is not less than or equal to `b`. In other words, for any element, there is another element that is either incomparable (not in a less-than-or-equal-to relation) or strictly smaller.
More concisely: For any type without a least element and a `LE` relation, each element has an element that is incomparable or strictly smaller.
|
IsBot.isMin
theorem IsBot.isMin : ∀ {α : Type u_1} [inst : LE α] {a : α}, IsBot a → IsMin a
The theorem `IsBot.isMin` states that for any type `α` that has a less than or equal to ordering (`LE`), if an element `a` of `α` is a bottom element (meaning it is less than or equal to every other element of `α`), then `a` is also a minimal element (meaning that there is no element strictly less than it). In other words, if `a` is at the bottom of the order, it also serves as a minimal bound for the set.
More concisely: If an element is the bottom element in a partially ordered type, then it is also a minimal element.
|
IsMin.ofDual
theorem IsMin.ofDual : ∀ {α : Type u_1} [inst : LE α] {a : αᵒᵈ}, IsMin a → IsMax (OrderDual.ofDual a)
This theorem, `IsMin.ofDual`, states that for any type `α` that has a less than or equal to ordering and any element `a` of the dual order of `α`, if `a` is a minimal element in the dual order, then the element of the original order corresponding to `a` via the identity function `OrderDual.ofDual` is a maximal element in the original order. In simpler terms, the minimal elements in the reversed order correspond to the maximal elements in the original order.
More concisely: For any type `α` with a valid ordering and any `a` in the dual ordering of `α`, `a` being minimal implies the element `OrderDual.ofDual a` in `α` is maximal.
|
NoMaxOrder.exists_gt
theorem NoMaxOrder.exists_gt : ∀ {α : Type u_3} [inst : LT α] [self : NoMaxOrder α] (a : α), ∃ b, a < b
This theorem states that for any type `α` that has a less than operation (`<`) and satisfies the property `NoMaxOrder`, for every individual element `a` of type `α`, there exists another element `b` such that `a` is less than `b`. In other words, there is no maximum element in a set defined with `NoMaxOrder`; for any given element, you can always find another one that is strictly greater.
More concisely: For any type `α` with a `<` relation and `NoMaxOrder` property, every element `a` has a strictly greater element `b`: `∀ (α : Type) [<_, DecidableRelation lt α], NoMaxOrder α → ∃ (b : α), a < b.`
|
not_isMin
theorem not_isMin : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : NoMinOrder α] (a : α), ¬IsMin a
The theorem `not_isMin` states that for any type `α` that has a preorder relationship and does not have a minimal element (expressed by the `NoMinOrder α` condition), no element `a` of type `α` can be a minimal element. This is to say, there is no element `a` in `α` such that for any other element `b` in `α`, if `b` is less than or equal to `a`, then `a` is less than or equal to `b`. The statement essentially defines a property of an ordered set without a minimum, where no element `a` can be a "minimal" element where no elements in the set are strictly less than `a`.
More concisely: In a preordered type `α` without a minimal element, there is no element that is minimal (i.e., less than or equal to every other element).
|
IsBot.toDual
theorem IsBot.toDual : ∀ {α : Type u_1} [inst : LE α] {a : α}, IsBot a → IsTop (OrderDual.toDual a)
The theorem `IsBot.toDual` states that for any type `α` with a less than or equal to (`LE`) relation and any element `a` of `α`, if `a` is a bottom element in `α` (meaning it is less than or equal to every other element in `α`) then the dual of `a` (obtained by the `OrderDual.toDual` function) is a top element in the dual order. In other words, if `a` is a least element in the original order, it becomes the greatest element when we consider the order reversed.
More concisely: If `a` is the bottom element in a type `α` with a `LE` relation, then the dual of `a` is the top element in the dual order.
|
NoMinOrder.exists_lt
theorem NoMinOrder.exists_lt : ∀ {α : Type u_3} [inst : LT α] [self : NoMinOrder α] (a : α), ∃ b, b < a
This theorem states that for every element `a` in a type `α` endowed with a less-than order structure, and assuming that the `α` has the property of not having a minimal element (NoMinOrder), there exists another element `b` such that `b` is strictly less than `a`. In Mathematical terms, it expresses that in a set without a minimal element, every element has at least one other element that is less than it.
More concisely: In a preorder type without a minimal element, every element has a strictly smaller element.
|
IsMax.eq_of_le
theorem IsMax.eq_of_le : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, IsMax a → a ≤ b → a = b
The theorem `IsMax.eq_of_le` states that for any partially ordered set `α`, if `a` is a maximal element in `α` (meaning that no element in `α` is strictly greater than `a`) and `a` is less than or equal to another element `b` in `α`, then `a` must be equal to `b`. This theorem captures the idea that in a partially ordered set, if an element is maximal and it is not strictly greater than another element, then these two elements must be the same.
More concisely: In a partially ordered set, if an element is maximal and less than or equal to another element, then they are equal.
|
IsMax.toDual
theorem IsMax.toDual : ∀ {α : Type u_1} [inst : LE α] {a : α}, IsMax a → IsMin (OrderDual.toDual a)
The theorem `IsMax.toDual` states that for any type `α` with a less-than-or-equal-to order (`≤`), if an element `a` is a maximal element in `α` (i.e., no element in `α` is strictly greater than `a`), then `a` is a minimal element in the dual order of `α` after applying the identity function `toDual` (i.e., no element in the dual order of `α` is strictly less than `a`). The term "dual order" refers to the order obtained by reversing the direction of the original order.
More concisely: If `α` is a type with a total order `≤`, and `a` is a maximal element in `α`, then `a` is a minimal element in the dual order of `α`.
|
IsTop.toDual
theorem IsTop.toDual : ∀ {α : Type u_1} [inst : LE α] {a : α}, IsTop a → IsBot (OrderDual.toDual a)
This theorem, `IsTop.toDual`, states that for any type `α` equipped with a less than or equal to order, if a certain element `a` of this type is a top element (meaning it is greater than or equal to any other element of `α`), then the dual order of `a` is a bottom element. Here, the dual order of `a` is simply `a` itself due to the identity function `OrderDual.toDual`. Therefore, it's essentially saying that if `a` is the largest element in the original order, it becomes the smallest element in the dual order.
More concisely: If `α` is a type equipped with a total order, and `a` is the greatest element in `α`, then `a` is the least element in the dual order of `α`.
|
IsTop.isMax
theorem IsTop.isMax : ∀ {α : Type u_1} [inst : LE α] {a : α}, IsTop a → IsMax a
This theorem states that for any type `α` equipped with a pre-order relation (denoted `LE α`), if an element `a` of `α` is a top element (as defined by the predicate `IsTop a`), then `a` is also a maximal element (`IsMax a`). In other words, if an element `a` is greater than or equal to any other element in the set, then there is no other element in the set which is strictly greater than `a`.
More concisely: For any type `α` with a pre-order relation `LE α`, if `a` is a top element (`IsTop a`), then `a` is maximal (`IsMax a`) in the sense that there is no `x` with `a < x` in `α`.
|
IsMin.not_lt
theorem IsMin.not_lt : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, IsMin a → ¬b < a
The theorem `IsMin.not_lt` states that for any type `α` equipped with a preorder, and any elements `a` and `b` of `α`, if `a` is a minimal element, then `b` is not strictly less than `a`. In other words, there does not exist an element `b` in `α` that is strictly less than a minimal element `a` in the preordered set `α`.
More concisely: If `α` is a preordered type and `a` is a minimal element of `α`, then there is no `b` in `α` such that `b` is strictly less than `a`.
|
LT.lt.not_isMax
theorem LT.lt.not_isMax : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a < b → ¬IsMax a
The theorem `LT.lt.not_isMax` states that for any type `α` that has a preorder relationship, if there exists an element `b` such that `a < b` for a certain `a`, then `a` is not a maximal element of `α`. In other words, if there is an element larger than `a`, then `a` cannot be the greatest element in the set.
More concisely: If `α` is a type with a preorder relation and there exists `b` such that `a < b`, then `a` is not a maximal element of `α`.
|
IsMin.eq_of_ge
theorem IsMin.eq_of_ge : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, IsMin a → b ≤ a → a = b
The theorem `IsMin.eq_of_ge` states that for any partially ordered type `α`, given two elements `a` and `b` of `α`, if `a` is a minimal element (meaning no other element is strictly less than `a`) and `b` is less than or equal to `a`, then `a` must be equal to `b`. Essentially, this theorem ensures that if `a` is a minimal element, there cannot exist another element that is less than or equal to `a` without being identical to `a`.
More concisely: If `α` is a partially ordered type, `a` is a minimal element of `α`, and `b ≤ a`, then `a = b`.
|
IsMin.toDual
theorem IsMin.toDual : ∀ {α : Type u_1} [inst : LE α] {a : α}, IsMin a → IsMax (OrderDual.toDual a)
The theorem `IsMin.toDual` states that for any type `α` which has an order structure, if a given element `a` is a minimal element of `α`, then the dual of `a` is a maximal element in the dual order of `α`. Here, the dual of an element is itself because the `OrderDual.toDual` function is an identity function, and the dual order is the reverse of the original order. In other words, if no elements are strictly less than `a` in `α`, then no elements are strictly greater than `a` in the reversed order of `α`.
More concisely: If `a` is the minimal element in an ordered type `α`, then the dual of `a` is the maximal element in the dual order of `α`.
|
not_isMax_iff
theorem not_isMax_iff : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, ¬IsMax a ↔ ∃ b, a < b
The theorem `not_isMax_iff` states that for any type `α` that has a preorder (a binary relation that is reflexive and transitive), an element `a` is not a maximal element if and only if there exists an element `b` such that `a` is strictly less than `b`. In other words, `a` is not the greatest element in `α` if we can find another element `b` in `α` that is bigger than `a`.
More concisely: For any preordered type `α` and element `a` in `α`, `a` is not a maximal element if and only if there exists `b` in `α` such that `a` is strictly preceded by `b` in the preorder relation.
|
not_isMin_iff
theorem not_isMin_iff : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, ¬IsMin a ↔ ∃ b, b < a
The theorem `not_isMin_iff` states that for any type `α` with a preorder relation, an element `a` of `α` is not a minimal element if and only if there exists an element `b` such that `b` is strictly less than `a`. Here, a minimal element is defined as an element `a` such that for all `b` in `α`, if `b` is less than or equal to `a`, then `a` is also less than or equal to `b`.
More concisely: For any preordered type `α`, an element `a` is not minimal if and only if there exists `b` in `α` with `b` strictly less than `a`.
|
not_isMax_of_lt
theorem not_isMax_of_lt : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a < b → ¬IsMax a
The theorem named `not_isMax_of_lt` states that for any preorder set `α` and any two elements `a` and `b` of this set, if `a` is strictly less than `b`, then `a` cannot be a maximal element of the set. In other words, there exists another element `b` that is strictly greater than `a`, thus `a` can't be the greatest element in the set `α`.
More concisely: If `α` is a preorder set and `a` is strictly less than `b` in `α`, then `a` cannot be a maximal element of `α`.
|
IsBot.ofDual
theorem IsBot.ofDual : ∀ {α : Type u_1} [inst : LE α] {a : αᵒᵈ}, IsBot a → IsTop (OrderDual.ofDual a)
The theorem `IsBot.ofDual` states that for any type `α` with a less than or equal to (`LE`) operation, and any element `a` in the dual order of `α`, if `a` is a bottom element in this dual order (i.e., `a` is less than or equal to any other element in the dual order), then the corresponding element in `α` obtained by applying the identity function `OrderDual.ofDual` to `a` is a top element in `α` (meaning it is greater than or equal to any other element in `α`). Essentially, it translates bottom elements in the dual order to top elements in the original order.
More concisely: For any type `α` with a `LE` order and any `a` being a bottom element in the dual order `α��rage`, the image `OrderDual.ofDual a` is a top element in the original order `α`.
|
IsMax.not_lt
theorem IsMax.not_lt : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, IsMax a → ¬a < b
The theorem `IsMax.not_lt` states that for any type `α` equipped with a preorder (that is, a binary relation that is reflexive and transitive), given any two elements `a` and `b` of type `α`, if `a` is a maximal element in `α` (i.e., no other element in `α` is strictly greater than `a`), then it is not the case that `a` is less than `b`. In other words, a maximal element `a` in a preordered set cannot be strictly less than any other element `b` from the same set.
More concisely: If `α` is a preordered type and `a` is a maximal element of `α`, then `a` is incomparable with any `b` in `α` such that `b` is strictly greater than `a`.
|
IsMax.eq_of_ge
theorem IsMax.eq_of_ge : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, IsMax a → a ≤ b → b = a
The theorem `IsMax.eq_of_ge` states that for any type `α` equipped with a partial order, if an element `a` is a maximal element and another element `b` satisfies the condition `a ≤ b`, then `b` must be equal to `a`. In other words, no element in the set can be strictly greater than a maximal element; if it's not less than the maximal element, then it must be equal.
More concisely: If `α` is a type equipped with a partial order, and `a` is a maximal element of `α` and `a ≤ b`, then `b = a`.
|
IsMax.ofDual
theorem IsMax.ofDual : ∀ {α : Type u_1} [inst : LE α] {a : αᵒᵈ}, IsMax a → IsMin (OrderDual.ofDual a)
This theorem, `IsMax.ofDual`, states that for any type `α` with a less-than-or-equal-to (`LE`) order, given a maximal element `a` of the dual order (`αᵒᵈ`), it also holds that the same element under the original `α` order is a minimal element when we apply the identity function `OrderDual.ofDual`. Simply put, if `a` is a maximal element in the reverse order, then it will be a minimal element in the original order.
More concisely: For any type `α` with a total order and any maximal element `a` in the dual order `αᵒᵈ`, `a` is a minimal element in the original order `α` under the function `OrderDual.ofDual`.
|
IsTop.ofDual
theorem IsTop.ofDual : ∀ {α : Type u_1} [inst : LE α] {a : αᵒᵈ}, IsTop a → IsBot (OrderDual.ofDual a)
The theorem `IsTop.ofDual` states that for any type `α` with a less than or equal to (`LE`) relation, if an element `a` (from the order dual of `α`, denoted as `αᵒᵈ`) is a top element (meaning it is greater than or equal to all other elements in `αᵒᵈ`), then the corresponding element in `α` obtained through the `OrderDual.ofDual` function is a bottom element in `α` (meaning it is less than or equal to all other elements in `α`). In other words, a top element in the order dual becomes a bottom element in the original order when we apply the `OrderDual.ofDual` function. This statement is essentially stating the reverse direction of the `isBot_ofDual_iff` theorem.
More concisely: For any type with a LE relation, the order dual of a top element is the corresponding bottom element in the original order.
|
LT.lt.not_isMin
theorem LT.lt.not_isMin : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, b < a → ¬IsMin a
This theorem states that for any ordered type `α`, if there exists an element `b` that is strictly less than `a` (`b < a`), then `a` cannot be a minimal element of `α`. In other words, if there is an element that is smaller than `a`, then `a` is not the smallest possible element in `α`.
More concisely: If an ordered type `α` has an element `b` such that `b < a`, then `a` is not the minimum element of `α`.
|
not_isMin_of_lt
theorem not_isMin_of_lt : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, b < a → ¬IsMin a
This theorem states that for any type `α` that has a preorder structure (a set equipped with a reflexive and transitive binary relation) and for any two elements `a` and `b` from that type, if `b` is strictly less than `a` then `a` cannot be a minimal element of `α`. Intuitively, this is saying that if there exists an element `b` that is strictly less than `a`, then `a` cannot be the smallest element in the set because there is at least one element `b` that is smaller.
More concisely: If `α` is a type with a preorder relation and `a` is an element of `α` such that there exists `b` in `α` with `b < a`, then `a` cannot be a minimal element of `α`.
|