Ordering.Compares.of_swap
theorem Ordering.Compares.of_swap :
∀ {α : Type u_1} [inst : LT α] {a b : α} {o : Ordering}, o.swap.Compares a b → o.Compares b a
This theorem, known as `Ordering.Compares.of_swap`, states that for any type `α` with a less-than (`LT`) relation, and any two instances `a` and `b` of this type, along with an `Ordering` `o`, if `o.swap` compares `a` to `b`, then `o` compares `b` to `a`. In simpler terms, this theorem assures that if `a` is less than, equal to, or greater than `b` according to the "swapped" ordering `o.swap`, then `b` is greater than, equal to, or less than `a` according to the original ordering `o`, respectively.
More concisely: If `o` is an ordering on type `α` such that `o.swap` compares `a` to `b`, then `o` compares `b` to `a` (i.e., `o.lt a b` if and only if `o.lt b a`).
|
Ordering.Compares.eq_lt
theorem Ordering.Compares.eq_lt :
∀ {α : Type u_1} [inst : Preorder α] {o : Ordering} {a b : α}, o.Compares a b → (o = Ordering.lt ↔ a < b) := by
sorry
The theorem `Ordering.Compares.eq_lt` states that for any given type `α` equipped with a preorder, an `Ordering` `o`, and elements `a` and `b` of type `α`, if `a` and `b` have the ordering relation `o` between them (as defined by `Ordering.Compares`), then `o` is equal to `Ordering.lt` if and only if `a` is less than `b`. In other words, the relation `a < b` is true exactly when the ordering `o` that compares `a` and `b` is `Ordering.lt`.
More concisely: If `α` is a type with preorder `o`, and `a` and `b` are elements of `α` with `a o b`, then `o = Ordering.lt` if and only if `a` is less than `b` (i.e., `a < b`).
|
Ordering.Compares.eq_eq
theorem Ordering.Compares.eq_eq :
∀ {α : Type u_1} [inst : Preorder α] {o : Ordering} {a b : α}, o.Compares a b → (o = Ordering.eq ↔ a = b) := by
sorry
The theorem `Ordering.Compares.eq_eq` states that for all types `α` that have an associated preorder relation, and for any instance of ordering `o` and two elements `a` and `b` of type `α`, if `a` and `b` have the ordering relation `o` between them, then `o` is equal to "equal" if and only if `a` is equal to `b`. In other words, this theorem establishes a correspondence between the equality of the ordering `o` to "equal" and the equality of the two elements `a` and `b` in the context of a preorder.
More concisely: For any preorder relation `o` on type `α`, if `a` and `b` have the ordering relation `o` and are equal, then `o` is the reflexive and symmetric relation equal to equality on `α`.
|
cmp_compares
theorem cmp_compares : ∀ {α : Type u_1} [inst : LinearOrder α] (a b : α), (cmp a b).Compares a b
This theorem, `cmp_compares`, states that for any type `α` with a linear order, and any two elements `a` and `b` of that type, the `cmp` function, which assigns an `Ordering` to the pair `(a, b)`, satisfies the `Ordering.Compares` property with respect to `a` and `b`. In other words, the relation between `a` and `b` indicated by the `Ordering` returned by `cmp a b` (less than, equal to, or greater than) accurately describes the actual relation between `a` and `b` according to their linear order.
More concisely: For any type `α` with a linear order and any `a, b : α`, the `cmp` function returns an `Ordering` that accurately reflects the comparison of `a` and `b` according to the linear order.
|
cmp_eq_cmp_symm
theorem cmp_eq_cmp_symm :
∀ {α : Type u_1} [inst : LinearOrder α] {x y : α} {β : Type u_3} [inst_1 : LinearOrder β] {x' y' : β},
cmp x y = cmp x' y' ↔ cmp y x = cmp y' x'
This theorem states that for any types `α` and `β` both equipped with a linear order, and any elements `x, y` of type `α` and `x', y'` of type `β`, the comparison (using 'less than' as defined by the cmp function) of `x` and `y` being the same as the comparison of `x'` and `y'` is equivalent to the comparison of `y` and `x` being the same as the comparison of `y'` and `x'`. This is effectively a statement of the symmetry of the comparison operation under swapping of the arguments.
More concisely: For all types `α` and `β` with linear orders, and all `x, y : α` and `x', y' : β`, `x < y <-> y' < x'`.
|
Ordering.Compares.swap
theorem Ordering.Compares.swap :
∀ {α : Type u_1} [inst : LT α] {a b : α} {o : Ordering}, o.Compares b a → o.swap.Compares a b
This theorem, `Ordering.Compares.swap`, is an alias of the reverse direction of `Ordering.compares_swap`. It's a statement applicable to any type `α` that has a less than (`LT`) operation defined. Given two elements `a` and `b` of this type `α`, and an `Ordering` `o` that compares `b` to `a`, this theorem asserts that upon swapping `a` and `b`, the swapped `o` will correctly compare `a` to `b`.
More concisely: If `o` is an ordering that compares `b` to `a`, then after swapping `a` and `b`, `o` will compare `a` to `b` in the reversed direction.
|
cmp_eq_eq_iff
theorem cmp_eq_eq_iff : ∀ {α : Type u_1} [inst : LinearOrder α] (x y : α), cmp x y = Ordering.eq ↔ x = y
This theorem states that for any type `α` that has a linear order, and for any two elements `x` and `y` of this type, the comparison of `x` and `y` using the function `cmp` (which compares two elements and returns an ordering) results in equality if and only if `x` and `y` are indeed equal. In other words, if `cmp x y` gives `Ordering.eq`, this means `x` is equal to `y` and vice versa.
More concisely: For any type `α` with a linear order, the function `cmp : α → α → Ordering` satisfies `cmp x y = Ordering.eq <-> x = y`.
|
lt_iff_lt_of_cmp_eq_cmp
theorem lt_iff_lt_of_cmp_eq_cmp :
∀ {α : Type u_1} [inst : LinearOrder α] {x y : α} {β : Type u_3} [inst_1 : LinearOrder β] {x' y' : β},
cmp x y = cmp x' y' → (x < y ↔ x' < y')
The theorem `lt_iff_lt_of_cmp_eq_cmp` states that for any two types `α` and `β`, both equipped with a linear order, and for any elements `x` and `y` from `α` and `x'` and `y'` from `β`, if the comparative orderings of `x` and `y` and `x'` and `y'` are the same, then `x` is less than `y` if and only if `x'` is less than `y'`. This provides a link between the relative orderings of two pairs of elements in potentially different ordered sets.
More concisely: For all types `α` and `β` with linear orders, and all elements `x` from `α`, `y` from `β`, `x'` from `α`, and `y'` from `β` such that `x` is related to `y` as `y` is to `x` if and only if `x'` is related to `y'` as `y'` is to `x'`, we have `x < y` if and only if `x' < y'`.
|