Mathlib.Order.SuccPred.Basic._auxLemma.15
theorem Mathlib.Order.SuccPred.Basic._auxLemma.15 :
∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : SuccOrder α] {a b : α} [inst_2 : NoMaxOrder α],
(Order.succ a = Order.succ b) = (a = b)
This theorem states that for any type `α` that has a partial order, successor order, and for which no maximal element exists, if the successor of an element `a` is equal to the successor of another element `b`, then `a` must be equal to `b`. The successor of an element is the least element greater than the given element if the given element is not maximal. If the element is maximal, its successor is the element itself.
More concisely: In a type `α` with no maximal element and having a successor order, if `a` and `b` have the same successor, then `a` equals `b`.
|
Order.le_of_pred_lt
theorem Order.le_of_pred_lt :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : PredOrder α] {a b : α}, Order.pred a < b → a ≤ b
This theorem states that for any given type `α` that has a preorder and predorder structure, and any two elements `a` and `b` of that type, if the predecessor of `a` is less than `b`, then `a` is less than or equal to `b`. Here, the predecessor of an element is the greatest element less than the given element, unless the element is minimal, in which case the predecessor is the element itself.
More concisely: For any type `α` with a preorder and a predorder structure, if the predecessor of element `a` is less than or equal to `b`, then `a` is less than or equal to `b`.
|
Order.succ_mono
theorem Order.succ_mono : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SuccOrder α], Monotone Order.succ
The theorem `Order.succ_mono` states that for any type `α` that has a preorder and a successor order structure, the successor function is monotone. In more detail, this means that if `a` and `b` are elements of type `α` and `a ≤ b`, then the successor of `a` is less than or equal to the successor of `b`. In mathematical terms, if `a ≤ b`, then `succ(a) ≤ succ(b)`. This theorem asserts the consistency of the successor operation within the ordered structure of the type.
More concisely: For any type with a preorder and successor order structure, the successor function is monotone, i.e., if `a ≤ b`, then `succ(a) ≤ succ(b)`.
|
CovBy.succ_eq
theorem CovBy.succ_eq :
∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : SuccOrder α] {a b : α}, a ⋖ b → Order.succ a = b
The theorem `CovBy.succ_eq` states that for any partially ordered set type `α`, endowed with a successor order, and any two elements `a` and `b` of type `α`, if `a` is covered by `b` (denoted `a ⋖ b`), then the successor of `a` is equal to `b`. In other words, if `b` is the least element greater than `a` (and no element exists between `a` and `b`), then `b` is the successor of `a`.
More concisely: If `a` is covered by `b` in a successor ordered set `α`, then `b` is the successor of `a` (i.e., `a < b` and there is no element `x` such that `a < x < b`).
|
Succ.rec
theorem Succ.rec :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SuccOrder α] [inst_2 : IsSuccArchimedean α] {P : α → Prop} {m : α},
P m → (∀ (n : α), m ≤ n → P n → P (Order.succ n)) → ∀ ⦃n : α⦄, m ≤ n → P n
The theorem `Succ.rec` is an induction principle for a type with a `SuccOrder`, namely, an order with a successor function. It applies to all elements above a given element `m` in a type `α` which is equipped with a Preorder and a SuccOrder, and also satisfies the `IsSuccArchimedean` property. The theorem asserts that if property `P` holds for `m`, and for any `n` greater than or equal to `m`, if `P` holds for `n` then it also holds for the successor of `n`, then `P` actually holds for all elements `n` that are greater than or equal to `m`.
More concisely: If `P` is a property that satisfies the hypotheses of `Succ.rec` in a type `α` with a `SuccOrder`, then `P` holds for all elements greater than or equal to `m` if it holds for `m` and for the successor of any element greater than or equal to `m`.
|
Order.le_pred_of_lt
theorem Order.le_pred_of_lt :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : PredOrder α] {a b : α}, a < b → a ≤ Order.pred b
This theorem states that for any type `α` that has a preorder and predecessor order structure, given any two elements `a` and `b` of type `α`, if `a` is less than `b`, then `a` is less than or equal to the predecessor of `b`. In other words, if `a` is strictly less than `b`, it is also less than or equal to the greatest element that is less than `b`. If `b` is a minimal element, then its predecessor is `b` itself, so `a` is less than or equal to `b`.
More concisely: For any preorder `α` with a predecessor order structure, if `a` is less than `b`, then `a` is less than or equal to the predecessor of `b`.
|
Order.pred_lt_iff_of_not_isMin
theorem Order.pred_lt_iff_of_not_isMin :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : PredOrder α] {a b : α}, ¬IsMin a → (Order.pred a < b ↔ a ≤ b) := by
sorry
The theorem `Order.pred_lt_iff_of_not_isMin` states that for any preorder type `α` with a defined predecessor order, and for any elements `a` and `b` of type `α`, if `a` is not a minimal element in `α`, then the predecessor of `a` is less than `b` if and only if `a` is less than or equal to `b`. Here, a minimal element is an element for which no other element is strictly less than it.
More concisely: For any preorder type `α` with a defined predecessor order, and any elements `a` and `b` of type `α`, if `a` is not minimal in `α`, then `a.predecessor < b` if and only if `a <= b`.
|
Order.succ_le_iff_of_not_isMax
theorem Order.succ_le_iff_of_not_isMax :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SuccOrder α] {a b : α}, ¬IsMax a → (Order.succ a ≤ b ↔ a < b) := by
sorry
The theorem `Order.succ_le_iff_of_not_isMax` states that for any preordered set `α` with a successor order, and any elements `a` and `b` in that set, if `a` is not a maximal element, then `Order.succ a ≤ b` if and only if `a < b`. In other words, the successor of `a` is less than or equal to `b` if and only if `a` itself is strictly less than `b`, given that `a` is not a maximal element in the set.
More concisely: For any preordered set with a successor order and elements `a` and `b`, `Order.succ a ≤ b` if and only if `a < b` when `a` is not maximal.
|
SuccOrder.max_of_succ_le
theorem SuccOrder.max_of_succ_le :
∀ {α : Type u_3} [inst : Preorder α] [self : SuccOrder α] {a : α}, SuccOrder.succ a ≤ a → IsMax a
This theorem states that for any type `α` that is equipped with a `Preorder` relation and a `SuccOrder` function, if the successor of an element `a` is less than or equal to `a` itself, then `a` is a maximal element of `α`. In other words, if there is no element strictly greater than `a` in `α`, and `a` is greater than or equal to its successor, then `a` is the greatest element in `α`.
More concisely: If a type `α` has a preorder relation and a `SuccOrder` function such that `a` has no strictly greater element and `a >= Succ a`, then `a` is the maximum element of `α`.
|
Order.succ_ne_succ
theorem Order.succ_ne_succ :
∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : SuccOrder α] {a b : α} [inst_2 : NoMaxOrder α],
a ≠ b → Order.succ a ≠ Order.succ b
The theorem `Order.succ_ne_succ` states that, for any type `α` equipped with a partial order and a successor operation (where "successor" is defined as the least element greater than a given one), if `α` does not have a maximal element, then distinct elements `a` and `b` of type `α` have distinct successors. In other words, if `a` and `b` are different, then their successors (the least elements greater than `a` and `b`, respectively) are also different.
More concisely: If a partial order on type `α` has no maximal element and is equipped with a successor operation, then distinct elements have distinct successors.
|
PredOrder.pred_le
theorem PredOrder.pred_le : ∀ {α : Type u_3} [inst : Preorder α] [self : PredOrder α] (a : α), PredOrder.pred a ≤ a
This theorem, `PredOrder.pred_le`, asserts that for all elements `a` of any type `α` that has a preorder and a predecessor order structure, the predecessor of `a` (`PredOrder.pred a`) is less than or equal to `a`. In other words, it establishes a basic ordering relationship with respect to the predecessor function in any preordered set.
More concisely: For all types `α` with a preorder and a predecessor order structure, the predecessor of any element `a` is less than or equal to `a`.
|
Order.lt_succ_of_not_isMax
theorem Order.lt_succ_of_not_isMax :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SuccOrder α] {a : α}, ¬IsMax a → a < Order.succ a
This theorem states that for any type `α` that has a preorder and successor order structure, if an element `a` of type `α` is not a maximal element (as defined by `IsMax`), then `a` is strictly less than the successor of `a` (as defined by `Order.succ`). In other words, if `a` is not the greatest element in its set, then the next element in the order is strictly greater than `a`.
More concisely: If `α` is a type with a preorder and successor structure, and `a` is an element of `α` that is not maximal, then `Order.succ a > a`.
|
Mathlib.Order.SuccPred.Basic._auxLemma.20
theorem Mathlib.Order.SuccPred.Basic._auxLemma.20 :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : PredOrder α] {a b : α} [inst_2 : NoMinOrder α],
(a ≤ Order.pred b) = (a < b)
This theorem states that for any type `α` that has a preorder and a predecessor order, and for any elements `a` and `b` of type `α` in a structure that has no minimum element, `a` being less than or equal to the predecessor of `b` is equivalent to `a` being less than `b`. In other words, if `α` is a type where we can talk about order and "the greatest element less than", and where there is no smallest element, then an element `a` is less than or equal to the "greatest element less than `b`" if and only if `a` is strictly less than `b`.
More concisely: For any type `α` with a preorder and a predecessor order and no minimum element, `a ≤ prev b` if and only if `a < b`.
|
Order.le_of_pred_le_pred
theorem Order.le_of_pred_le_pred :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : PredOrder α] {a b : α} [inst_2 : NoMinOrder α],
Order.pred a ≤ Order.pred b → a ≤ b
This theorem, referred to as "Alias of the forward direction of `Order.pred_le_pred_iff`", states that given a type `α` which has a preorder and predorder structure, and for any two elements `a` and `b` of this type such that the type does not contain a minimal element (`NoMinOrder α`), if the predecessor of `a` is less than or equal to the predecessor of `b` (`Order.pred a ≤ Order.pred b`), then `a` is also less than or equal to `b` (`a ≤ b`). "Predecessor" here refers to the greatest element that is less than the given element, or the element itself if it's minimal.
More concisely: If `α` is a type with no minimal element and `Order.pred a ≤ Order.pred b` in a preorder and predorder structure on `α`, then `a ≤ b`.
|
SuccOrder.succ_le_of_lt
theorem SuccOrder.succ_le_of_lt :
∀ {α : Type u_3} [inst : Preorder α] [self : SuccOrder α] {a b : α}, a < b → SuccOrder.succ a ≤ b
This theorem, `SuccOrder.succ_le_of_lt`, states that for all types `α` that have a preorder and a successor order defined, and for all elements `a` and `b` of type `α`, if `a` is less than `b`, then the successor of `a` is less than or equal to `b`. Essentially, it ensures that the successor function respects the ordering invariants between 'less than' and 'less than or equal to' in the context of the type `α`.
More concisely: For all types `α` with preorder and successor order, if `a` < `b`, then `a+1` ≤ `b`.
|
Order.pred_lt_of_not_isMin
theorem Order.pred_lt_of_not_isMin :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : PredOrder α] {a : α}, ¬IsMin a → Order.pred a < a
The theorem `Order.pred_lt_of_not_isMin` states that, for any type `α` that has a preorder and predorder structure, if an element `a` of type `α` is not minimal, then the predecessor of `a` is strictly less than `a`. In more mathematical terms, the theorem says that if `a` is not a minimal element in the order, then its predecessor is strictly smaller than `a`. This theorem is essentially the reverse direction of the theorem `Order.pred_lt_iff_not_isMin`.
More concisely: If `α` is a type with a preorder and predorder structure, then for all `a` in `α` that are not minimal, `pred a` is strictly less than `a`.
|
Order.le_succ
theorem Order.le_succ : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SuccOrder α] (a : α), a ≤ Order.succ a := by
sorry
The theorem `Order.le_succ` states that for any type `α` equipped with a preorder and a successor order, any element `a` of type `α` is less than or equal to its successor. In other words, given any element `a` in the set, it is either less than or equal to the next element in the ordered sequence (its successor). If `a` is a maximal element, then `a` is equal to its successor; otherwise, its successor is greater than `a`.
More concisely: For any type `α` with a preorder and a successor order, for all `a` in `α`, `a ≤ a.successor`.
|
PredOrder.le_pred_of_lt
theorem PredOrder.le_pred_of_lt :
∀ {α : Type u_3} [inst : Preorder α] [self : PredOrder α] {a b : α}, a < b → a ≤ PredOrder.pred b
This theorem states that for any type `α` that has a preorder relation and a defined predecessor operation, if an element `a` of type `α` is less than another element `b` of the same type, then `a` is also less than or equal to the predecessor of `b`. In other words, if `a` is strictly less than `b`, then `a` must be less than or equal to the element that comes immediately before `b` in the defined ordering of type `α`.
More concisely: If `α` is a type with a preorder relation and a defined predecessor operation, then for all `a` and `b` in `α`, if `a` is strictly less than `b`, then `a` is less than or equal to the predecessor of `b`.
|
Order.lt_succ_iff_of_not_isMax
theorem Order.lt_succ_iff_of_not_isMax :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SuccOrder α] {a b : α}, ¬IsMax a → (b < Order.succ a ↔ b ≤ a) := by
sorry
The theorem `Order.lt_succ_iff_of_not_isMax` states that for any preorder type `α` that also has a defined successor operation, and for any two elements `a` and `b` of type `α`, if `a` is not a maximal element, then `b` is less than the successor of `a` if and only if `b` is less than or equal to `a`. In other words, if an element is not the greatest in the order, then any other element is less than the successor of the first element just when it is less than or equal to that first element itself.
More concisely: For any preorder type `α` with a successor operation, if `a` is not the maximum element, then `b ≤ a` if and only if `b < succ a`.
|
Order.lt_of_succ_lt_succ
theorem Order.lt_of_succ_lt_succ :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SuccOrder α] {a b : α} [inst_2 : NoMaxOrder α],
Order.succ a < Order.succ b → a < b
This theorem, referred to as an "alias" of the forward direction of `Order.succ_lt_succ_iff`, asserts that for any given type `α` equipped with a preorder and successor order, and for any two elements `a` and `b` of `α` in a system where there is no maximum order, if the successor of `a` is less than the successor of `b`, it implies that `a` is less than `b`. In other words, the relationship of 'less than' is preserved under the operation of taking successors in such a system.
More concisely: If `α` is a type with a preorder and successor order such that there is no maximum, then `a < b` implies `succ a < succ b`.
|
Order.le_of_succ_le_succ
theorem Order.le_of_succ_le_succ :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SuccOrder α] {a b : α} [inst_2 : NoMaxOrder α],
Order.succ a ≤ Order.succ b → a ≤ b
This theorem, named `Order.le_of_succ_le_succ`, states that for any type `α` with a preorder and a successor order such that it has no maximal element, if the successor of an element `a` is less than or equal to the successor of an element `b`, then `a` is less than or equal to `b`. Essentially, it says that if the next item after `a` is not greater than the next item after `b`, then `a` cannot be greater than `b`. This is a forward direction alias of the theorem `Order.succ_le_succ_iff`.
More concisely: If `α` is a type with no maximal element and `a` and `b` are elements of `α` such that `a < succ b` or `succ a <= succ b`, then `a <= b`.
|
Order.Iic_pred_of_not_isMin
theorem Order.Iic_pred_of_not_isMin :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : PredOrder α] {a : α},
¬IsMin a → Set.Iic (Order.pred a) = Set.Iio a
The theorem `Order.Iic_pred_of_not_isMin` states that for any type `α` equipped with a preorder and a predecessor order, and for any element `a` of that type which is not a minimal element (meaning there exists some other element that is strictly less than `a`), the left-closed right-infinite interval ending at `a`'s predecessor (`Set.Iic (Order.pred a)`) is equivalent to the left-open right-infinite interval ending at `a` (`Set.Iio a`). In other words, if `a` is not minimal, then all elements less than or equal to `a`'s predecessor are exactly those elements that are strictly less than `a`.
More concisely: For any preordered type `α` and `a` not minimal in it, `Set.Iic (Order.pred a)` equals `Set.Iio a`.
|
Order.Iio_succ
theorem Order.Iio_succ :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SuccOrder α] [inst_2 : NoMaxOrder α] (a : α),
Set.Iio (Order.succ a) = Set.Iic a
This theorem states that for any type `α` that is preordered, has an operation for finding the successor of an element (`SuccOrder`), and does not have a maximum element (`NoMaxOrder`), the left-infinite right-open interval ending at the successor of any element `a` is the same as the left-infinite right-closed interval ending at `a`. In simpler terms, the set of elements less than the successor of `a` is identical to the set of elements less than or equal to `a`.
More concisely: For any preordered type `α` without a maximum element, the left-open interval `(−∞, Succ a)` is equal to the left-closed interval `[−∞, a]`.
|
Order.lt_succ_bot_iff
theorem Order.lt_succ_bot_iff :
∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : SuccOrder α] {a : α} [inst_2 : OrderBot α]
[inst_3 : NoMaxOrder α], a < Order.succ ⊥ ↔ a = ⊥
This theorem states that for any type `α` which has a partial order, a successor order, a least element (denoted by `⊥`), and no maximal element, an element `a` of this type is less than the successor of `⊥` if and only if `a` is equal to `⊥`. Here, the successor of an element is the least element that is greater than the element, unless the element is a maximal element, in which case its successor is the element itself.
More concisely: For any type with a partial order, successor, least element, and no maximal element, an element is less than the successor of the least element if and only if it is equal to the least element.
|
Order.max_of_succ_le
theorem Order.max_of_succ_le :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SuccOrder α] {a : α}, Order.succ a ≤ a → IsMax a
The theorem `Order.max_of_succ_le` states that for any type `α` that has a preordering and a successor order, if the successor of an element `a` is less than or equal to `a`, then `a` is a maximal element of `α`. Here, `a` being a maximal element means that there is no element in `α` that is strictly greater than `a`.
More concisely: If `α` is a type with a preordering and a successor order, and `a` is an element of `α` with `a ≤ succ a`, then `a` is the maximum element of `α`.
|
Order.succ_le_iff
theorem Order.succ_le_iff :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SuccOrder α] {a b : α} [inst_2 : NoMaxOrder α],
Order.succ a ≤ b ↔ a < b
This theorem, `Order.succ_le_iff`, states that for any type `α` equipped with a preorder and a successor order (where we can define a "next" element, the successor, for any element of the type), and given two elements `a` and `b` of this type such that `α` has no maximal element, `a` is strictly less than `b` if and only if the successor of `a` is less than or equal to `b`. In other words, the successor of `a` being less than or equal to `b` is equivalent to `a` being strictly less than `b`.
More concisely: For any type equipped with a preorder and a successor order without a maximal element, `a` strictly less than `b` if and only if the successor of `a` is less than or equal to `b`.
|
SuccOrder.le_of_lt_succ
theorem SuccOrder.le_of_lt_succ :
∀ {α : Type u_3} [inst : Preorder α] [self : SuccOrder α] {a b : α}, a < SuccOrder.succ b → a ≤ b
This theorem states that for any type `α` that has an associated Preorder and SuccOrder, and for any two elements `a` and `b` of this type, if `a` is less than the successor of `b`, then `a` is also less than or equal to `b`. In other words, if `a` is less than what comes after `b`, then `a` must also be less than or, at most, equal to `b`.
More concisely: If `α` is a type with Preorder and SuccOrder, then for all `a` and `b` in `α`, if `a` < Succ `b`, then `a` ≤ `b`.
|
Order.min_of_le_pred
theorem Order.min_of_le_pred :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : PredOrder α] {a : α}, a ≤ Order.pred a → IsMin a
This theorem states that for any type `α` that has a preordering and predorder structure, if an element `a` of type `α` is less than or equal to its predecessor, then `a` is a minimal element of `α`. Here, an element is said to be minimal if there is no element strictly less than it. The predecessor of an element `a` is the greatest element less than `a` if `a` is not minimal; if `a` is minimal, then its predecessor is `a` itself.
More concisely: If `α` is a type with a preordering and `a` is an element of `α` such that `a` is less than or equal to its predecessor, then `a` is a minimal element of `α`.
|
CovBy.pred_eq
theorem CovBy.pred_eq :
∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : PredOrder α] {a b : α}, a ⋖ b → Order.pred b = a
This theorem, `CovBy.pred_eq`, states that for any given type `α` which has a partial order and a predecessor order, and any two elements `a` and `b` of this type, if `a` is covered by `b` (denoted as `a ⋖ b` meaning `a < b ∧ ¬∃ c, a < c ∧ c < b`), then the predecessor of `b` (computed with `Order.pred b`) is equal to `a`. Essentially, if `b` directly follows `a` in the order, then `a` is identified as the predecessor of `b`.
More concisely: If `a` is covered by `b` in a partially ordered type, then `Order.pred b = a`.
|
IsMax.succ_eq
theorem IsMax.succ_eq :
∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : SuccOrder α] {a : α}, IsMax a → Order.succ a = a
The theorem `IsMax.succ_eq` states that for any type `α` equipped with a partial order and a successor order, if an element `a` of `α` is maximal (meaning that no other element in `α` is strictly greater than `a`), then the successor of `a` is `a` itself. In other words, if `a` is a maximal element, then there's no element strictly greater than `a`, hence the successor of `a` is `a`. This theorem is an alias of the reverse direction of `Order.succ_eq_iff_isMax`.
More concisely: If `α` is a type equipped with partial and successor orders, then for all `a` in `α`, if `a` is maximal, then `a = succ a`.
|
Order.succ_le_of_lt
theorem Order.succ_le_of_lt :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SuccOrder α] {a b : α}, a < b → Order.succ a ≤ b
The theorem `Order.succ_le_of_lt` states that for any given preorder set `α` with a successor order and any two elements `a` and `b` from `α`, if `a` is less than `b`, then the successor of `a` is less than or equal to `b`. In other words, if `a` is strictly less than `b`, then the next element after `a` in the order (or `a` itself if `a` is the maximal element) is not greater than `b`.
More concisely: For any preorder set with a successor order, if `a` is less than `b`, then `a.successor` is less than or equal to `b`.
|
Order.covBy_succ
theorem Order.covBy_succ :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SuccOrder α] [inst_2 : NoMaxOrder α] (a : α), a ⋖ Order.succ a := by
sorry
This theorem states that for any type `α` that has a preorder (i.e., a relation that is reflexive and transitive), a successor order (i.e., a function that assigns to each element a successor), and no maximal element, every element `a` of this type is covered by its successor. Here, "covered" (`⋖`) means that `a` is less than its successor and there is no element strictly between `a` and its successor.
More concisely: In a preorder type without maximal elements, every element is covered by its successor.
|
Order.succ_lt_succ
theorem Order.succ_lt_succ :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SuccOrder α] {a b : α} [inst_2 : NoMaxOrder α],
a < b → Order.succ a < Order.succ b
This theorem, `Order.succ_lt_succ`, is an alias of the converse of `Order.succ_lt_succ_iff`. It states that for any type `α` that has a preorder and successor order and does not have a maximal element, if a given element `a` is less than another element `b`, then the successor of `a` is less than the successor of `b`. The successor of an element is defined as the least element greater than it if the element is not maximal; if the element is maximal, its successor is itself.
More concisely: For any type `α` with a preorder and successor order and no maximal element, if `a < b`, then `a.successor < b.successor`.
|
Order.pred_ne_pred
theorem Order.pred_ne_pred :
∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : PredOrder α] {a b : α} [inst_2 : NoMinOrder α],
a ≠ b → Order.pred a ≠ Order.pred b
This theorem, referred to as `Order.pred_ne_pred`, is an alternate form of the converse of `Order.pred_ne_pred_iff` in the context of order theory. It states that for any set `α` with a specified partial order and predecessor order, and any two different elements `a` and `b` from this set where `α` has no minimal element, the predecessor of `a` is not equal to the predecessor of `b`. In other words, distinct elements in a partially ordered set without a minimum element have distinct predecessors.
More concisely: In a partially ordered set without a minimum element, distinct elements have distinct predecessors.
|
Order.covBy_succ_of_not_isMax
theorem Order.covBy_succ_of_not_isMax :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SuccOrder α] {a : α}, ¬IsMax a → a ⋖ Order.succ a
The theorem `Order.covBy_succ_of_not_isMax` states that for any type `α` that has a preorder structure and a successor order, given any element `a` of type `α` that is not a maximal element, `a` is covered by its successor. In other words, there is no element of type `α` that is strictly greater than `a` and strictly less than the successor of `a`. Symbolically, if `a` is not a maximal element, then `a ⋖ Order.succ a`, where `⋖` denotes the covering relation.
More concisely: If `α` is a preordered type with a successor order and `a` is not a maximal element of `α`, then there is no element strictly between `a` and the successor of `a`.
|
Pred.rec
theorem Pred.rec :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : PredOrder α] [inst_2 : IsPredArchimedean α] {P : α → Prop} {m : α},
P m → (∀ n ≤ m, P n → P (Order.pred n)) → ∀ ⦃n : α⦄, n ≤ m → P n
This theorem provides an induction principle for a type with a `PredOrder`, meaning there is a way to define the "predecessor" of an element, for all elements below a given element `m`. Specifically, it states that for any type `α` with a preorder and a `PredOrder`, if a property `P` holds true for `m` and for any `n` less than or equal to `m`, if `P` holds for `n` then it also holds for the predecessor of `n`, then `P` will hold for all `n` less than or equal to `m`. This is a type of mathematical induction that works 'backward', from a maximum `m` down to all elements below it in the order.
More concisely: If `α` is a type with a preorder and a `PredOrder`, and `P(m)` holds for all `m` and for all `n` less than or equal to `m` with `P(n)` implying `P(pred n)`, then `P` holds for all `n` less than or equal to `m`.
|
SuccOrder.le_succ
theorem SuccOrder.le_succ : ∀ {α : Type u_3} [inst : Preorder α] [self : SuccOrder α] (a : α), a ≤ SuccOrder.succ a
This theorem states that for any preordered set `α` that has a successor function, every element `a` in `α` is less than or equal to its successor. In other words, given a preordered set (one where the elements have an ordering that is reflective, transitive, and antisymmetric), and a successor function that maps an element to its subsequent element, the theorem assures that any element `a` in this set won't exceed its successor. This is a foundational property in structures with a successor operation, including the natural numbers under standard ordering.
More concisely: In a preordered set with a successor function, every element is less than or equal to its successor under the given ordering.
|
LE.le.exists_succ_iterate
theorem LE.le.exists_succ_iterate :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SuccOrder α] [inst_2 : IsSuccArchimedean α] {a b : α},
a ≤ b → ∃ n, Order.succ^[n] a = b
This theorem states that for any type `α` equipped with a pre-order structure and a successor function, and assuming that the successor function satisfies the Archimedean property, given any two elements `a` and `b` of type `α` such that `a` is less than or equal to `b`, there exists a natural number `n` such that iteratively applying the successor function to `a` `n` times yields `b`. In other words, you can reach `b` from `a` by repeatedly applying the successor function a certain number of times.
More concisely: Given a pre-order type `α` with a successor function satisfying the Archimedean property, for all `a` and `b` in `α` with `a ≤ b`, there exists a natural number `n` such that `a successor^n = b`.
|
Order.Iio_succ_eq_insert_of_not_isMax
theorem Order.Iio_succ_eq_insert_of_not_isMax :
∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : SuccOrder α] {a : α},
¬IsMax a → Set.Iio (Order.succ a) = insert a (Set.Iio a)
This theorem states that for any partially ordered type `α` which also has a defined successor operation, given any element `a` of `α` that is not a maximal element, the left-infinite right-open interval up to the successor of `a` is equal to the set obtained by inserting `a` into the left-infinite right-open interval up to `a`. In more informal terms, if `a` is not the largest possible element, then all elements less than the next element after `a` are the same as all elements less than `a`, plus `a` itself.
More concisely: For any partially ordered type `α` with a successor operation, if `a` is an element of `α` that is not maximal, then the set of elements strictly less than the successor of `a` is equal to the set of elements strictly less than `a` union `{a}`.
|
Mathlib.Order.SuccPred.Basic._auxLemma.9
theorem Mathlib.Order.SuccPred.Basic._auxLemma.9 :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SuccOrder α] {a b : α} [inst_2 : NoMaxOrder α],
(Order.succ a ≤ b) = (a < b)
This theorem, `Mathlib.Order.SuccPred.Basic._auxLemma.9`, states that for any type `α` with a predefined preorder and successor order, and where maximum elements do not exist (`NoMaxOrder α`), for any two elements `a` and `b` of type `α`, the statement "`a` is strictly less than `b`" is equivalent to the statement "the successor of `a` is less than or equal to `b`".
More concisely: For any type `α` without maximum elements and equipped with a preorder and successor order, `a` is strictly less than `b` if and only if `a <*: Succ a ≤ b`, where `<:*` denotes the preorder and `Succ` is the successor function.
|
Order.pred_covBy_of_not_isMin
theorem Order.pred_covBy_of_not_isMin :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : PredOrder α] {a : α}, ¬IsMin a → Order.pred a ⋖ a
The theorem `Order.pred_covBy_of_not_isMin` states that for every type `α` with a preorder and predecessor order, for any element `a` of `α` that is not a minimal element (i.e., there exists another element in `α` that is strictly less than `a`), the predecessor of `a` (which is the greatest element less than `a`) is strictly less than `a`. In terms of relations, this theorem says that if `a` is not the least element in its set, then its predecessor is strictly less than `a`.
More concisely: If `α` is a type with a preorder and `a` is an element of `α` that is not minimal, then `pred a` (the predecessor of `a`) is strictly less than `a`.
|
IsMin.pred_eq
theorem IsMin.pred_eq :
∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : PredOrder α] {a : α}, IsMin a → Order.pred a = a
This theorem states that for any type `α` that has a partial order and a predecessor order, and for any element `a` of type `α`, if `a` is a minimal element (meaning no element is strictly less than it), then the predecessor of `a` is `a` itself. This essentially means that for minimal elements, the predecessor operation leaves the element unchanged.
More concisely: For any type `α` with a partial order and a predecessor function, if `a` is a minimal element, then `pred a = a`.
|
Order.lt_of_pred_lt_pred
theorem Order.lt_of_pred_lt_pred :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : PredOrder α] {a b : α} [inst_2 : NoMinOrder α],
Order.pred a < Order.pred b → a < b
This theorem, referred to as the "Alias" of the forward direction of `Order.pred_lt_pred_iff`, states that for any ordered type `α` that is subject to a preorder relation and a predecessor order, if an element `a` and `b` of `α` exist such that `a` is not the minimal element of `α` and the predecessor of `a` is less than the predecessor of `b`, then `a` is less than `b`. In simpler terms, if the predecessor of `a` is smaller than the predecessor of `b`, then `a` is also smaller than `b`.
More concisely: If `α` is an ordered type subject to a preorder relation and `a` and `b` are elements of `α` such that `a` is not minimal and `pred a < pred b`, then `a < b`.
|
Order.succ_le_succ
theorem Order.succ_le_succ :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SuccOrder α] {a b : α}, a ≤ b → Order.succ a ≤ Order.succ b := by
sorry
The theorem `Order.succ_le_succ` states that for any type `α` which has a pre-order and successor relation, if an element `a` is less than or equal to an element `b`, then the successor of `a` is less than or equal to the successor of `b`. In mathematical terms, this can be stated as `∀ a, b ∈ α, a ≤ b → succ(a) ≤ succ(b)`, where `succ` denotes the successor function.
More concisely: For any type `α` with pre-order and successor relation, the successor of a lesser element is lesser than the successor of a greater element: `∀ a b : α, a ≤ b → succ(a) ≤ succ(b)`.
|
Order.pred_lt_pred
theorem Order.pred_lt_pred :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : PredOrder α] {a b : α} [inst_2 : NoMinOrder α],
a < b → Order.pred a < Order.pred b
The theorem `Order.pred_lt_pred` is an alias for the reverse direction of the theorem `Order.pred_lt_pred_iff`. It states that for any type `α` that has a preorder and a predecessor order, and for any two elements `a` and `b` of that type such that `α` does not have a minimal element, if `a` is less than `b`, then the predecessor of `a` is less than the predecessor of `b`.
More concisely: For types with a preorder and a predecessor order and no minimal element, if `a < b`, then `pred a < pred b`.
|
PredOrder.le_of_pred_lt
theorem PredOrder.le_of_pred_lt :
∀ {α : Type u_3} [inst : Preorder α] [self : PredOrder α] {a b : α}, PredOrder.pred a < b → a ≤ b
The theorem `PredOrder.le_of_pred_lt` states that for every type `α` that has a preorder and a predecessor order defined on it, for any two elements `a` and `b` of type `α`, if the predecessor of `a` is less than `b`, then `a` is less than or equal to `b`. This theorem is essentially verifying that the predecessor function `pred` adheres to the ordering invariants between the "less than or equal" (`LE`) and "less than" (`LT`) relations in the given order structure.
More concisely: For any type `α` with a preorder and a predecessor order, `pred a < b` implies `a <= b`.
|
Order.bot_lt_succ
theorem Order.bot_lt_succ :
∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : SuccOrder α] [inst_2 : OrderBot α] [inst_3 : Nontrivial α]
(a : α), ⊥ < Order.succ a
This theorem states that, for any type `α` that has a partial order, a successor order, a least element (`OrderBot`), and is nontrivial (i.e., has at least two distinct elements), the least element of this type is less than the successor of any element in this type. In other words, for any element `a` of the type `α`, the successor of `a` is always greater than the least element of `α`.
More concisely: For any type `α` with a partial order, a successor function, a least element `OrderBot`, and at least two elements, `OrderBot` is less than every successor element.
|
IsPredArchimedean.exists_pred_iterate_of_le
theorem IsPredArchimedean.exists_pred_iterate_of_le :
∀ {α : Type u_3} [inst : Preorder α] [inst_1 : PredOrder α] [self : IsPredArchimedean α] {a b : α},
a ≤ b → ∃ n, Order.pred^[n] b = a
The theorem `IsPredArchimedean.exists_pred_iterate_of_le` states that for any type `α` that has a preorder and a predecessor order, and for any instances `a` and `b` of type `α` such that `a` is less than or equal to `b`, there exists a natural number `n` such that if we apply the predecessor function (`Order.pred`) `n` times on `b`, we arrive at `a`. This is under the assumption that the type `α` satisfies the IsPredArchimedean property, which means we can reach any value in the order by iteratively applying the predecessor function.
More concisely: For any type `α` with a preorder and a predecessor order that satisfies the IsPredArchimedean property, there exists a natural number `n` such that `Order.pred^n(b) = a` for any `a ≤ b` in `α`.
|
Order.pred_mono
theorem Order.pred_mono : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : PredOrder α], Monotone Order.pred
The theorem `Order.pred_mono` states that for any type `α` that has a `Preorder` and a `PredOrder` structure, the predecessor function `Order.pred` is monotone. In other words, if `a` and `b` are elements of `α` and `a ≤ b`, then `Order.pred a ≤ Order.pred b`, where `Order.pred a` and `Order.pred b` are the greatest elements less than `a` and `b` respectively, or equal to `a` and `b` if they are minimal.
More concisely: For all types `α` with `Preorder` and `PredOrder` structures, the predecessor function `Order.pred` is monotone, that is, `Order.pred a ≤ Order.pred b` whenever `a ≤ b`.
|
PredOrder.min_of_le_pred
theorem PredOrder.min_of_le_pred :
∀ {α : Type u_3} [inst : Preorder α] [self : PredOrder α] {a : α}, a ≤ PredOrder.pred a → IsMin a
This theorem states that for any type `α` that has a Preorder and PredOrder structure, if an element `a` from `α` is less than or equal to its predecessor (`PredOrder.pred a`), then `a` is a minimal element of `α`. In other words, no other element in `α` is strictly less than `a`.
More concisely: If `α` is a type with Preorder and PredOrder structures, then `a ≤ Pred a` implies that `a` is a minimal element of `α`. In other words, for any `α` with these structures, if `a` is preceded by an element `Pred a`, then `a` has no strictly smaller elements in `α`.
|
Mathlib.Order.SuccPred.Basic._auxLemma.8
theorem Mathlib.Order.SuccPred.Basic._auxLemma.8 :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SuccOrder α] {a b : α} [inst_2 : NoMaxOrder α],
(a < Order.succ b) = (a ≤ b)
This theorem states that for any type `α` endowed with a preorder and a successor order (where the successor of an element is defined as the least element greater than the given element or the element itself if it is maximal), and a pair of elements `a` and `b` of type `α` in a context where no maximal order is defined, the proposition that `a` is less than the successor of `b` is equivalent to the proposition that `a` is less than or equal to `b`.
More concisely: In a preordered type `α` with a successor order and no maximal element, for all `a` and `b` in `α`, `a` is less than the successor of `b` if and only if `a` is less than or equal to `b`.
|
IsSuccArchimedean.exists_succ_iterate_of_le
theorem IsSuccArchimedean.exists_succ_iterate_of_le :
∀ {α : Type u_3} [inst : Preorder α] [inst_1 : SuccOrder α] [self : IsSuccArchimedean α] {a b : α},
a ≤ b → ∃ n, Order.succ^[n] a = b
This theorem, named `IsSuccArchimedean.exists_succ_iterate_of_le`, states that for any given type `α` equipped with a preorder and a successor order (where the successor of an element `a` is the least element greater than `a` if `a` is not maximal, otherwise it is `a` itself), if `a` is less than or equal to `b` (`a ≤ b`), then there exists a non-negative integer `n` such that iterating the successor function `n` times on `a` yields `b` (`Order.succ^[n] a = b`). This theorem is a statement of Archimedean property for the `succ` function.
More concisely: For any preordered type equipped with a successor order, if `a` is less than or equal to `b`, then there exists a non-negative integer `n` such that `Order.succ^[n] a = b`. (This is the Archimedean property for the successor function.)
|
Mathlib.Order.SuccPred.Basic._auxLemma.19
theorem Mathlib.Order.SuccPred.Basic._auxLemma.19 :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : PredOrder α] {a b : α} [inst_2 : NoMinOrder α],
(Order.pred a < b) = (a ≤ b)
This theorem states that for any type `α` which has a preorder and a predecessor order, and for any elements `a` and `b` of this type, if `α` also has no minimal element (NoMinOrder), then the predecessor of `a` is less than `b` if and only if `a` is less than or equal to `b`. This essentially establishes a relationship between the predecessor order and the standard preorder in the given context.
More concisely: If `α` is a type with a preorder and a predecessor order and no minimal element, then `a < b` if and only if `a <= b` or `a = b` for any `a, b : α`.
|
Order.succ_injective
theorem Order.succ_injective :
∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : SuccOrder α] [inst_2 : NoMaxOrder α],
Function.Injective Order.succ
The theorem `Order.succ_injective` states that for any type `α` equipped with a partial order, a successor order, and without a maximum element (`NoMaxOrder α`), the function `Order.succ`, which assigns to each element its successor, is injective. In other words, if `Order.succ a = Order.succ b` for some `a` and `b` in `α`, then `a = b`. This essentially means that different elements in `α` have different successors in the context of the given orderings.
More concisely: In a partially ordered type without a maximum element, the successor function is injective.
|
Order.Ici_succ_of_not_isMax
theorem Order.Ici_succ_of_not_isMax :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SuccOrder α] {a : α},
¬IsMax a → Set.Ici (Order.succ a) = Set.Ioi a
The theorem `Order.Ici_succ_of_not_isMax` states that for any type `α` with a preorder and successor order, and any element `a` of `α`, if `a` is not a maximal element, then the left-closed right-infinite interval starting at the successor of `a` (`Set.Ici (Order.succ a)`) is equal to the left-open right-infinite interval starting just after `a` (`Set.Ioi a`).
In other words, if `a` is not the greatest element, the set of all elements greater than or equal to the next element after `a` is the same as the set of all elements strictly greater than `a`.
More concisely: If `α` is a type with a preorder and successor order, and `a` is not the greatest element of `α`, then `Set.Ici (Order.succ a)` equals `Set.Ioi a`.
|
Order.le_succ_iff_eq_or_le
theorem Order.le_succ_iff_eq_or_le :
∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : SuccOrder α] {a b : α},
a ≤ Order.succ b ↔ a = Order.succ b ∨ a ≤ b
The theorem `Order.le_succ_iff_eq_or_le` states that for any partially ordered type `α` that also has a successor function and any two elements `a` and `b` of type `α`, `a` is less than or equal to the successor of `b` if and only if `a` is equal to the successor of `b` or `a` is less than or equal to `b`. This theorem bridges the relation between the successor function and the order relation.
More concisely: For any partially ordered type with a successor function, the order relation holds between elements `a` and the successor of `b` if and only if `a` is equal to the successor of `b` or `a` is less than or equal to `b`.
|
Order.succ_le_succ_iff
theorem Order.succ_le_succ_iff :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SuccOrder α] {a b : α} [inst_2 : NoMaxOrder α],
Order.succ a ≤ Order.succ b ↔ a ≤ b
The theorem `Order.succ_le_succ_iff` states that for any type `α` that is a preorder and has a successor order with no maximum element, for any two elements `a` and `b` of this type, the successor of `a` is less than or equal to the successor of `b` if and only if `a` is less than or equal to `b`. In other words, in such a structure, the order of elements is preserved when taking successors.
More concisely: For any preorder type `α` without a maximum element having a successor order, `a ≤ b` if and only if `succ a ≤ succ b`.
|
Order.le_of_lt_succ
theorem Order.le_of_lt_succ :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SuccOrder α] {a b : α}, a < Order.succ b → a ≤ b
This theorem states that for any type `α` equipped with a preorder and a successor function, and for any elements `a` and `b` of that type, if `a` is less than the successor of `b`, then `a` is less than or equal to `b`. In mathematical terms, given `a < succ(b)`, we can infer `a ≤ b`. The successor function here is defined with respect to the order, and if `b` is not a maximal element, `succ(b)` is the smallest element greater than `b`. If `b` is maximal, then `succ(b) = b`.
More concisely: For any type with a preorder and a successor function, if `a` is strictly less than the successor of `b`, then `a` is less than or equal to `b`.
|
Order.Ioi_pred_of_not_isMin
theorem Order.Ioi_pred_of_not_isMin :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : PredOrder α] {a : α},
¬IsMin a → Set.Ioi (Order.pred a) = Set.Ici a
The theorem `Order.Ioi_pred_of_not_isMin` states that for any type `α` that has a preorder and a predecessor order, and for any element `a` of that type, if `a` is not a minimal element, then the interval of all elements strictly greater than the predecessor of `a` (`Set.Ioi (Order.pred a)`) is equal to the interval of all elements greater than or equal to `a` (`Set.Ici a`). In other words, if `a` is not the smallest element in the set, then the set of all elements larger than what comes just before `a` is the same as the set of all elements that are larger or equal to `a`.
More concisely: For any type `α` with a preorder and a predecessor order, if `a` is not the least element, then `Set.Ioi (Order.pred a) = Set.Ici a`.
|
Order.pred_le
theorem Order.pred_le : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : PredOrder α] (a : α), Order.pred a ≤ a := by
sorry
The theorem `Order.pred_le` states that for any type `α`, given that `α` is equipped with a Preorder and a PredOrder structure, the predecessor of any element `a` from `α` is less than or equal to `a` itself. In other words, for any element `a` in a preordered set, the element `Order.pred a`, which is defined as the greatest element less than `a` if `a` is not minimal and as `a` itself if `a` is minimal, is always less than or equal to `a`.
More concisely: For any preordered type `α` and element `a` in `α`, the predecessor `Order.pred a` satisfies `Order.pred a ≤ a`.
|
Order.lt_succ_iff
theorem Order.lt_succ_iff :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SuccOrder α] {a b : α} [inst_2 : NoMaxOrder α],
a < Order.succ b ↔ a ≤ b
This theorem, `Order.lt_succ_iff`, states that for any type `α` that has a pre-order and successor order structure, and for any elements `a` and `b` of this type where the type does not have a maximal element, `a` is less than the successor of `b` if and only if `a` is less than or equal to `b`. This essentially describes a fundamental property of the "successor" operation in the context of ordered sets without a maximum element.
More concisely: For any type `α` with a pre-order and successor order structure and no maximum element, `a < succ(b)` if and only if `a ≤ b`.
|
Order.lt_succ
theorem Order.lt_succ :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SuccOrder α] [inst_2 : NoMaxOrder α] (a : α), a < Order.succ a := by
sorry
This theorem, `Order.lt_succ`, states that for any type `α` equipped with a preorder and a successor relation, and assuming that `α` does not have a maximal element, any element `a` of type `α` is strictly less than its successor. In other words, for any given element `a`, the successor of `a`, denoted as `Order.succ a`, is always greater than `a`.
More concisely: For any type `α` with a preorder and successor relation having no maximal element, every element `a` satisfies `a < Order.succ a`.
|
Order.succ_eq_iff_covBy
theorem Order.succ_eq_iff_covBy :
∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : SuccOrder α] {a b : α} [inst_2 : NoMaxOrder α],
Order.succ a = b ↔ a ⋖ b
This theorem states that for any type `α` equipped with a partial order and a successor order, and for any elements `a` and `b` of the type `α` in a space without a maximal element, the successor of `a` equals `b` if and only if `a` is covered by `b`. Here, 'covered by' is denoted by the symbol `⋖`, which means that `a` is less than `b` and there is no element `c` such that `a` is less than `c` and `c` is less than `b`.
More concisely: For any type `α` with a partial order and successor order, without a max element, `a ⋖ b` if and only if `a = Suc(b)`, where `Suc` denotes the successor function.
|
Order.Iio_succ_of_not_isMax
theorem Order.Iio_succ_of_not_isMax :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SuccOrder α] {a : α},
¬IsMax a → Set.Iio (Order.succ a) = Set.Iic a
The theorem `Order.Iio_succ_of_not_isMax` states that, for any preorder type `α` that also has a successor order and any element `a` of type `α`, if `a` is not a maximal element of `α` (meaning there exists an element in `α` that is strictly greater than `a`), then the left-infinite right-open interval less than the successor of `a` (denoted `Set.Iio (Order.succ a)`) is equal to the left-infinite right-closed interval less than or equal to `a` (denoted `Set.Iic a`). In other words, if `a` is not the highest value in the set, then all values less than the next highest value are also all the values less than or equal to `a`.
More concisely: If `α` is a preorder type with a successor order and `a` is an element of `α` not maximally bounded above, then `Set.Iio (Order.succ a) = Set.Iic a`.
|