LT.lt.dual
theorem LT.lt.dual : ∀ {α : Type u_1} [inst : LT α] {a b : α}, b < a → OrderDual.toDual a < OrderDual.toDual b := by
sorry
The theorem `LT.lt.dual` is an alias for the reverse direction of the theorem `OrderDual.toDual_lt_toDual`. It states that for any type `α` that has a less than (`LT`) operation and any two elements `a` and `b` of `α`, if `b` is less than `a`, then `a` in the dual order is less than `b` in the dual order. Basically, it says that the "less than" relation in the original order is reversed in the dual order.
More concisely: If `a` is less than `b` in the original order, then `b` is less than `a` in the dual order.
|
OrderDual.toDual_le_toDual
theorem OrderDual.toDual_le_toDual :
∀ {α : Type u_1} [inst : LE α] {a b : α}, OrderDual.toDual a ≤ OrderDual.toDual b ↔ b ≤ a
The theorem `OrderDual.toDual_le_toDual` states that for all types `α` that have a less than or equal to (`≤`) relation, and for any two elements `a` and `b` from `α`, the inequality `OrderDual.toDual a ≤ OrderDual.toDual b` holds if and only if `b ≤ a`. In other words, the function `OrderDual.toDual` effectively reverses the order of the original less than or equal to relation.
More concisely: For any type equipped with a reflexive, transitive, and antisymmetric relation `≤`, the dual relation `OrderDual.toDual` satisfies `a ≤ b <-> OrderDual.toDual b <= OrderDual.toDual a`.
|
LE.le.dual
theorem LE.le.dual : ∀ {α : Type u_1} [inst : LE α] {a b : α}, b ≤ a → OrderDual.toDual a ≤ OrderDual.toDual b := by
sorry
This theorem, referred to as `LE.le.dual`, states that for any type `α` that possesses a less than or equal to (`≤`) relation, if `b` is less than or equal to `a` (represented as `b ≤ a`), then the OrderDual of `a` is less than or equal to the OrderDual of `b` in the `OrderDual` of `α` (represented as `OrderDual.toDual a ≤ OrderDual.toDual b`). In other words, this theorem is saying that the order relation is reversed in the dual of a linear order.
More concisely: For any type `α` with a `≤` relation, if `b ≤ a`, then `OrderDual.toDual a ≤ OrderDual.toDual b`. In other words, the order relation is reversed in the dual of a linear order.
|
Mathlib.Order.Synonym._auxLemma.5
theorem Mathlib.Order.Synonym._auxLemma.5 :
∀ {α : Type u_1} {p : αᵒᵈ → Prop}, (∀ (a : αᵒᵈ), p a) = ∀ (a : α), p (OrderDual.toDual a)
The theorem `Mathlib.Order.Synonym._auxLemma.5` states that for any type `α` and any property `p` that takes as input elements of the order dual of `α` (symbolized as `αᵒᵈ`), saying that "the property `p` holds for all elements `a` of `αᵒᵈ`" is equivalent to stating "for all elements `a` of `α`, the property `p` holds for `a` when it is transformed into its order dual using the function `OrderDual.toDual`". In essence, it shows the property preservation under the transformation to the order dual.
More concisely: The theorem `Mathlib.Order.Synonym._auxLemma.5` asserts that for any property `p` on the order dual `αᵒᵈ` of a type `α`, `p` holds for all elements `a` in `αᵒᵈ` if and only if it holds for the order duals `OrderDual.toDual a` of all elements `a` in `α`.
|
LE.le.ofDual
theorem LE.le.ofDual : ∀ {α : Type u_1} [inst : LE α] {a b : αᵒᵈ}, b ≤ a → OrderDual.ofDual a ≤ OrderDual.ofDual b := by
sorry
This theorem, denoted as `LE.le.ofDual`, states that for any type `α` that has a `LE` (less than or equal to) instance, given any two elements `a` and `b` from the OrderDual of `α` (denoted as `αᵒᵈ`), if `b` is less than or equal to `a` in the dual order, then the elements obtained by applying the `OrderDual.ofDual` function to `a` and `b` respectively are also in the same order relation. In other words, the theorem establishes the reverse direction of the inequality after applying the identity function `OrderDual.ofDual` on `a` and `b`.
More concisely: For any type `α` with an `LE` instance and elements `a` and `b` in the OrderDual of `α`, if `b ≤ a` in the dual order, then `OrderDual.ofDual a ≤ OrderDual.ofDual b`.
|
OrderDual.ofDual_le_ofDual
theorem OrderDual.ofDual_le_ofDual :
∀ {α : Type u_1} [inst : LE α] {a b : αᵒᵈ}, OrderDual.ofDual a ≤ OrderDual.ofDual b ↔ b ≤ a
The theorem `OrderDual.ofDual_le_ofDual` states that for any type `α`, which has an order relation, and any two elements `a` and `b` of the dual of `α`, the element `a` is less than or equal to `b` in the dual order if and only if `b` is less than or equal to `a` in the original order. In essence, this theorem states that the `OrderDual.ofDual` function reverses the order relation.
More concisely: For any type `α` with an order relation and any of its dual elements `a` and `b`, `a ≤ b` in the dual order if and only if `b ≤ a` in the original order.
|
LT.lt.ofDual
theorem LT.lt.ofDual : ∀ {α : Type u_1} [inst : LT α] {a b : αᵒᵈ}, b < a → OrderDual.ofDual a < OrderDual.ofDual b := by
sorry
This theorem, referred to as `LT.lt.ofDual`, asserts that for any type `α` that has a less-than (`LT`) relation, and any two elements `a` and `b` of the dual order of `α`, if `b` is less than `a` in the dual order, then `a` is less than `b` in the original order once we apply the identity function `OrderDual.ofDual`. In simpler terms, this theorem states that the less-than relation in the dual order is reversed when we map back to the original order.
More concisely: For any type `α` with a `LT` relation and dual order `OrderDual α`, if `b` is less than `a` in the dual order `OrderDual α`, then `a` is less than `b` in the original order `LT α` after applying the function `OrderDual.ofDual`. In other words, `OrderDual.ofDual (lt b a) ↔ ¬ lt a b` for `LT α` and `OrderDual α`.
|