Order.IsSuccLimit.succ_lt
theorem Order.IsSuccLimit.succ_lt :
∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : SuccOrder α] {a b : α},
Order.IsSuccLimit b → a < b → Order.succ a < b
This theorem, `Order.IsSuccLimit.succ_lt`, states that for any partially ordered set `α` that also has a successor order, given any two elements `a` and `b` of this set, if `b` is a successor limit (meaning there's no element that is less than `b` but not equal to `b`), and `a` is less than `b`, then the successor of `a` is still less than `b`. In simpler terms, even if we move to the next element after `a`, we still haven't reached `b`, given that `b` is a successor limit and `a` is less than `b`.
More concisely: If `α` is a partially ordered set with a successor order, `a` is an element less than the successor limit `b` in `α`, then `a.succ` is also less than `b`.
|
Order.isSuccLimit_toDual_iff
theorem Order.isSuccLimit_toDual_iff :
∀ {α : Type u_1} [inst : LT α] {a : α}, Order.IsSuccLimit (OrderDual.toDual a) ↔ Order.IsPredLimit a
This theorem states that for any type `α` with a less than (`LT`) operation and any element `a` of this type, `a` is a successor limit in the dual order if and only if `a` is a predecessor limit in the original order. Here, a successor limit is a value that does not cover any other in a successor order, meaning it cannot be the successor of anything smaller. Conversely, a predecessor limit is a value that is not covered by any other in a predecessor order, implying it cannot be the predecessor of anything greater. The function `OrderDual.toDual` is used to transform an element from the original order type to the equivalent in the dual order.
More concisely: For any type with a total order and an element, it is a successor limit in the dual order if and only if it is a predecessor limit in the original order.
|
Order.isSuccLimit.dual
theorem Order.isSuccLimit.dual :
∀ {α : Type u_1} [inst : LT α] {a : α}, Order.IsSuccLimit a → Order.IsPredLimit (OrderDual.toDual a)
This theorem, `Order.isSuccLimit.dual`, states that for any type `α` that has a less than operation, if an element `a` of `α` is a successor limit (i.e., there is no element `b` in `α` such that `b` is strictly less than `a`), then `a` is a predecessor limit in the dual order, which is obtained by reversing the less than operation. In other words, there is no element `b` in the dual order such that `a` is strictly less than `b`.
More concisely: If `a` is a successor limit in the order `<` on type `α`, then `a` is a predecessor limit in the dual order `>` on `α`.
|
Order.isSuccLimit_of_succ_lt
theorem Order.isSuccLimit_of_succ_lt :
∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : SuccOrder α] {b : α},
(∀ a < b, Order.succ a < b) → Order.IsSuccLimit b
The theorem `Order.isSuccLimit_of_succ_lt` states that for any type `α` with a partial order and a successor order, if for any element `a` that is less than a given element `b`, the successor of `a` is also less than `b`, then `b` is a successor limit. In other words, `b` is a successor limit if it is not the successor of any element that is less than it.
More concisely: If for all `a` such that `a < b` in a partially ordered type `α`, it holds that `a < succ(b)`, then `b` is a successor limit.
|
Order.mem_range_pred_of_not_isPredLimit
theorem Order.mem_range_pred_of_not_isPredLimit :
∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : PredOrder α] {a : α},
¬Order.IsPredLimit a → a ∈ Set.range Order.pred
The theorem `Order.mem_range_pred_of_not_isPredLimit` states that for any element `a` in a partial order that is not a predecessor limit, `a` is in the range of the predecessor function. In other words, if there is another value in the order that precedes `a`, then `a` is the successor of some value in the order, and thus falls in the set of values obtained by applying the predecessor function to all elements in the order.
More concisely: If an element in a partial order is not a predecessor limit, then it is in the range of the predecessor function.
|
Order.isPredLimitRecOn.proof_1
theorem Order.isPredLimitRecOn.proof_1 :
∀ {α : Type u_1} [inst : PartialOrder α] (x : αᵒᵈ), Order.IsSuccLimit x → Order.IsPredLimit (OrderDual.toDual x)
The theorem `Order.isPredLimitRecOn.proof_1` states that for any type `α` that has a partial order, if an element `x` in the dual of the ordered set `α` is a successor limit (meaning there is no other element in the set that is less than `x` and close to `x`), then the dual of `x` is a predecessor limit in the original ordered set (meaning there is no other element in the set that is greater than the dual of `x` and close to the dual of `x`).
More concisely: If `x` is a successor limit in the dual of a partially ordered type `α`, then the dual of `x` is a predecessor limit in `α`.
|
IsMin.isSuccLimit
theorem IsMin.isSuccLimit : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, IsMin a → Order.IsSuccLimit a
The theorem `IsMin.isSuccLimit` states that for any type `α` with a preorder structure, if an element `a` of `α` is a minimal element (i.e., there is no other element in `α` that is strictly smaller than `a`), then `a` is also a successor limit. In other words, no element `b` in `α` is strictly less than `a` and also covers `a`. Hence, `a` cannot be the successor of anything smaller.
More concisely: If an element is minimal in a preordered type, then it has no strictly smaller covering elements.
|
Order.isPredLimit.dual
theorem Order.isPredLimit.dual :
∀ {α : Type u_1} [inst : LT α] {a : α}, Order.IsPredLimit a → Order.IsSuccLimit (OrderDual.toDual a)
This theorem, `Order.isPredLimit.dual`, states that for any type `α` with a less than structure (`LT α`), if a given element `a` of that type is a predecessor limit, then the dual of `a` is a successor limit. Here, a "predecessor limit" is defined as a value that isn't less than any other value, while a "successor limit" is a value that isn't greater than any other value. The operation `OrderDual.toDual` is simply returning the dual element `a` in the order dual of `α`.
More concisely: If `a` is a predecessor limit in the ordered type `α`, then the dual of `a` is a successor limit in the order dual of `α`.
|
Order.IsSuccLimit.isMax
theorem Order.IsSuccLimit.isMax :
∀ {α : Type u_1} [inst : Preorder α] {a : α} [inst_1 : SuccOrder α], Order.IsSuccLimit (Order.succ a) → IsMax a
The theorem `Order.IsSuccLimit.isMax` states that for all types `α` that have a pre-order and a successor order, if for any element `a` of `α`, the successor of `a` is a successor limit (which means that it doesn't cover any element smaller than itself), then `a` is a maximal element. Here, `a` is considered a maximal element if there is no element strictly greater than it in the set `α`.
More concisely: If every successor element in a pre-ordered type with a successor order is a successor limit and has no greater element, then it is a maximal element.
|
Order.not_isSuccLimit_iff
theorem Order.not_isSuccLimit_iff :
∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : SuccOrder α] {a : α},
¬Order.IsSuccLimit a ↔ ∃ b, ¬IsMax b ∧ Order.succ b = a
This theorem states that for any type `α` equipped with a partial order and a successor order, and for any element `a` of `α`, the property that `a` is not a successor limit is equivalent to the existence of some element `b` such that `b` is not maximal and the successor of `b` is `a`.
In more layman's terms, an element is not a successor limit if and only if there is another element that is not the largest in the order and, when moved one step further in the order, reaches the original element. This bridges the concepts of successor limit, maximality, and successor operation in this particular order structure.
More concisely: For any type `α` with partial and successor orders, an element `a` is not a successor limit if and only if there exists a non-maximal element `b` such that the successor of `b` is `a`.
|
Order.mem_range_succ_of_not_isSuccLimit
theorem Order.mem_range_succ_of_not_isSuccLimit :
∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : SuccOrder α] {a : α},
¬Order.IsSuccLimit a → a ∈ Set.range Order.succ
The theorem `Order.mem_range_succ_of_not_isSuccLimit` states that for any type `α` equipped with a partial order and a successor order, if a given element `a` of type `α` is not a successor limit (meaning there exists some other element `b` such that `b` is strictly less than `a`), then `a` is an element in the range of the successor function. In other words, if `a` is not a successor limit, there exists another element in the set such that `a` is the successor of that element.
More concisely: If `α` is a type equipped with a partial order and a successor function, and there exists `b` such that `b` is strictly less than `a` in `α`, then `a` is in the range of the successor function.
|