mathlib documentation

order.order_dual

Initial lemmas to work with the order_dual #

Definitions #

to_dual and of_dual the order reversing identity maps, bundled as equivalences.

Basic Lemmas to convert between an order and its dual #

This file is similar to algebra/group/type_tags.lean

source
@[protected, instance]
def order_dual.nontrivial {α : Type u} [nontrivial α] :
nontrivial (order_dual α)
source
def order_dual.to_dual {α : Type u} :
α ≃ order_dual α

to_dual is the identity function to the order_dual of a linear order.

Equations
source
def order_dual.of_dual {α : Type u} :
order_dual α ≃ α

of_dual is the identity function from the order_dual of a linear order.

Equations
source
@[simp]
theorem order_dual.to_dual_symm_eq {α : Type u} :
order_dual.to_dual.symm = order_dual.of_dual
source
@[simp]
theorem order_dual.of_dual_symm_eq {α : Type u} :
order_dual.of_dual.symm = order_dual.to_dual
source
@[simp]
theorem order_dual.to_dual_of_dual {α : Type u} (a : order_dual α) :
⇑order_dual.to_dual (⇑order_dual.of_dual a) = a
source
@[simp]
theorem order_dual.of_dual_to_dual {α : Type u} (a : α) :
⇑order_dual.of_dual (⇑order_dual.to_dual a) = a
source
@[simp]
theorem order_dual.to_dual_inj {α : Type u} {a b : α} :
⇑order_dual.to_dual a = ⇑order_dual.to_dual b ↔ a = b
source
@[simp]
theorem order_dual.to_dual_le_to_dual {α : Type u} [has_le α] {a b : α} :
⇑order_dual.to_dual a ≤ ⇑order_dual.to_dual b ↔ b ≤ a
source
@[simp]
theorem order_dual.to_dual_lt_to_dual {α : Type u} [has_lt α] {a b : α} :
⇑order_dual.to_dual a < ⇑order_dual.to_dual b ↔ b < a
source
@[simp]
theorem order_dual.of_dual_inj {α : Type u} {a b : order_dual α} :
⇑order_dual.of_dual a = ⇑order_dual.of_dual b ↔ a = b
source
@[simp]
theorem order_dual.of_dual_le_of_dual {α : Type u} [has_le α] {a b : order_dual α} :
⇑order_dual.of_dual a ≤ ⇑order_dual.of_dual b ↔ b ≤ a
source
@[simp]
theorem order_dual.of_dual_lt_of_dual {α : Type u} [has_lt α] {a b : order_dual α} :
⇑order_dual.of_dual a < ⇑order_dual.of_dual b ↔ b < a
source
theorem order_dual.le_to_dual {α : Type u} [has_le α] {a : order_dual α} {b : α} :
a ≤ ⇑order_dual.to_dual b ↔ b ≤ ⇑order_dual.of_dual a
source
theorem order_dual.lt_to_dual {α : Type u} [has_lt α] {a : order_dual α} {b : α} :
a < ⇑order_dual.to_dual b ↔ b < ⇑order_dual.of_dual a
source
theorem order_dual.to_dual_le {α : Type u} [has_le α] {a : α} {b : order_dual α} :
⇑order_dual.to_dual a ≤ b ↔ ⇑order_dual.of_dual b ≤ a
source
theorem order_dual.to_dual_lt {α : Type u} [has_lt α] {a : α} {b : order_dual α} :
⇑order_dual.to_dual a < b ↔ ⇑order_dual.of_dual b < a
source
@[protected]
def order_dual.rec {α : Type u} {C : order_dual α → Sort u_1} (h₂ : Π (a : α), C (⇑order_dual.to_dual a)) (a : order_dual α) :
C a

Recursor for order_dual α.

Equations
source
@[protected, simp]
theorem order_dual.forall {α : Type u} {p : order_dual α → Prop} :
(∀ (a : order_dual α), p a) ↔ ∀ (a : α), p (⇑order_dual.to_dual a)
source
@[protected, simp]
theorem order_dual.exists {α : Type u} {p : order_dual α → Prop} :
(∃ (a : order_dual α), p a) ↔ ∃ (a : α), p (⇑order_dual.to_dual a)
source
theorem has_lt.lt.dual {α : Type u} [has_lt α] {a b : α} :
b < a → ⇑order_dual.to_dual a < ⇑order_dual.to_dual b

Alias of order_dual.to_dual_lt_to_dual.

source
theorem has_le.le.dual {α : Type u} [has_le α] {a b : α} :
b ≤ a → ⇑order_dual.to_dual a ≤ ⇑order_dual.to_dual b

Alias of order_dual.to_dual_le_to_dual.