Order dual

This file defines OrderDual α, a type synonym reversing the meaning of all inequalities, with notation αᵒᵈ.

Notation

αᵒᵈ is notation for OrderDual α.

Implementation notes

One should not abuse definitional equality between α and αᵒᵈ. Instead, explicit coercions should be inserted:

• OrderDual.toDual : α → αᵒᵈ and OrderDual.ofDual : αᵒᵈ → α

def OrderDual (α : Type u_2) : Type u_2

Type synonym to equip a type with the dual order: ≤ means ≥ and < means >. αᵒᵈ is notation for OrderDual α.

def «term_ᵒᵈ» : Lean.TrailingParserDescr

Type synonym to equip a type with the dual order: ≤ means ≥ and < means >. αᵒᵈ is notation for OrderDual α.

instance OrderDual.instNonempty (α : Type u_2) [h : Nonempty α] : Nonempty αᵒᵈ

instance OrderDual.instSubsingleton (α : Type u_2) [h : Subsingleton α] : Subsingleton αᵒᵈ

@[implicit_reducible]

instance OrderDual.instLE (α : Type u_2) [h : LE α] : LE αᵒᵈ

@[implicit_reducible]

instance OrderDual.instLT (α : Type u_2) [h : LT α] : LT αᵒᵈ

@[implicit_reducible]

instance OrderDual.instOrd (α : Type u_2) [h : Ord α] : Ord αᵒᵈ

@[implicit_reducible]

instance OrderDual.instMaxOfMin (α : Type u_2) [h : Min α] : Max αᵒᵈ

@[implicit_reducible]

instance OrderDual.instMinOfMax (α : Type u_2) [h : Max α] : Min αᵒᵈ

instance OrderDual.instIsTransLe {α : Type u_1} [LE α] [T : IsTrans α LE.le] : IsTrans αᵒᵈ LE.le

instance OrderDual.instIsTransLt {α : Type u_1} [LT α] [T : IsTrans α LT.lt] : IsTrans αᵒᵈ LT.lt

instance OrderDual.instTrichotomousLt {α : Type u_1} [LT α] [T : Std.Trichotomous LT.lt] : Std.Trichotomous LT.lt

@[implicit_reducible]

instance OrderDual.instPreorder (α : Type u_2) [Preorder α] : Preorder αᵒᵈ

@[implicit_reducible]

instance OrderDual.instPartialOrder (α : Type u_2) [PartialOrder α] : PartialOrder αᵒᵈ

@[implicit_reducible]

instance OrderDual.instDecidableEq (α : Type u_2) [DecidableEq α] : DecidableEq αᵒᵈ

@[implicit_reducible]

instance OrderDual.instDecidableLT (α : Type u_2) [LT α] [h : DecidableLT α] : DecidableLT αᵒᵈ

@[implicit_reducible]

instance OrderDual.instDecidableLE (α : Type u_2) [LE α] [h : DecidableLE α] : DecidableLE αᵒᵈ

@[implicit_reducible]

instance OrderDual.instLinearOrder (α : Type u_2) [LinearOrder α] : LinearOrder αᵒᵈ

@[implicit_reducible]

def LinearOrder.swap (α : Type u_2) : LinearOrder α → LinearOrder α

The opposite linear order to a given linear order

@[implicit_reducible]

instance OrderDual.instInhabited {α : Type u_1} [h : Inhabited α] : Inhabited αᵒᵈ

theorem OrderDual.Ord.dual_dual (α : Type u_2) [H : Ord α] : instOrd αᵒᵈ = H

theorem OrderDual.Preorder.dual_dual (α : Type u_2) [H : Preorder α] : instPreorder αᵒᵈ = H

theorem OrderDual.instPartialOrder.dual_dual (α : Type u_2) [H : PartialOrder α] : instPartialOrder αᵒᵈ = H

theorem OrderDual.instLinearOrder.dual_dual (α : Type u_2) [H : LinearOrder α] : instLinearOrder αᵒᵈ = H

instance OrderDual.instNontrivial {α : Type u_1} [h : Nontrivial α] : Nontrivial αᵒᵈ

@[implicit_reducible]

instance OrderDual.instUnique {α : Type u_1} [h : Unique α] : Unique αᵒᵈ

def OrderDual.toDual {α : Type u_1} : α ≃ αᵒᵈ

toDual is the identity function to the OrderDual of a linear order.

def OrderDual.ofDual {α : Type u_1} : αᵒᵈ ≃ α

ofDual is the identity function from the OrderDual of a linear order.

@[simp]

theorem OrderDual.toDual_symm_eq {α : Type u_1} : toDual.symm = ofDual

@[simp]

theorem OrderDual.ofDual_symm_eq {α : Type u_1} : ofDual.symm = toDual

@[simp]

theorem OrderDual.toDual_ofDual {α : Type u_1} (a : αᵒᵈ) : toDual (ofDual a) = a

@[simp]

theorem OrderDual.ofDual_toDual {α : Type u_1} (a : α) : ofDual (toDual a) = a

@[simp]

theorem OrderDual.toDual_trans_ofDual {α : Type u_1} : toDual.trans ofDual = Equiv.refl α

@[simp]

theorem OrderDual.ofDual_trans_toDual {α : Type u_1} : ofDual.trans toDual = Equiv.refl αᵒᵈ

@[simp]

theorem OrderDual.toDual_comp_ofDual {α : Type u_1} : ⇑toDual ∘ ⇑ofDual = id

@[simp]

theorem OrderDual.ofDual_comp_toDual {α : Type u_1} : ⇑ofDual ∘ ⇑toDual = id

theorem OrderDual.toDual_inj {α : Type u_1} {a b : α} : toDual a = toDual b ↔ a = b

theorem OrderDual.ofDual_inj {α : Type u_1} {a b : αᵒᵈ} : ofDual a = ofDual b ↔ a = b

theorem OrderDual.ext {α : Type u_1} {a b : αᵒᵈ} (h : ofDual a = ofDual b) : a = b

theorem OrderDual.ext_iff {α : Type u_1} {a b : αᵒᵈ} : a = b ↔ ofDual a = ofDual b

@[simp]

theorem OrderDual.toDual_le_toDual {α : Type u_1} [LE α] {a b : α} : toDual a ≤ toDual b ↔ b ≤ a

@[simp]

theorem OrderDual.toDual_lt_toDual {α : Type u_1} [LT α] {a b : α} : toDual a < toDual b ↔ b < a

@[simp]

theorem OrderDual.ofDual_le_ofDual {α : Type u_1} [LE α] {a b : αᵒᵈ} : ofDual a ≤ ofDual b ↔ b ≤ a

@[simp]

theorem OrderDual.ofDual_lt_ofDual {α : Type u_1} [LT α] {a b : αᵒᵈ} : ofDual a < ofDual b ↔ b < a

theorem OrderDual.le_toDual {α : Type u_1} [LE α] {a : αᵒᵈ} {b : α} : a ≤ toDual b ↔ b ≤ ofDual a

theorem OrderDual.toDual_le {α : Type u_1} [LE α] {a : αᵒᵈ} {b : α} : toDual b ≤ a ↔ ofDual a ≤ b

theorem OrderDual.lt_toDual {α : Type u_1} [LT α] {a : αᵒᵈ} {b : α} : a < toDual b ↔ b < ofDual a

theorem OrderDual.toDual_lt {α : Type u_1} [LT α] {a : αᵒᵈ} {b : α} : toDual b < a ↔ ofDual a < b

def OrderDual.rec {α : Type u_1} {motive : αᵒᵈ → Sort u_2} (toDual : (a : α) → motive (toDual a)) (a : αᵒᵈ) : motive a

Recursor for αᵒᵈ.

@[simp]

theorem OrderDual.forall {α : Type u_1} {p : αᵒᵈ → Prop} : (∀ (a : αᵒᵈ), p a) ↔ ∀ (a : α), p (toDual a)

@[simp]

theorem OrderDual.exists {α : Type u_1} {p : αᵒᵈ → Prop} : (∃ (a : αᵒᵈ), p a) ↔ ∃ (a : α), p (toDual a)

theorem LE.le.dual {α : Type u_1} [LE α] {a b : α} : b ≤ a → OrderDual.toDual a ≤ OrderDual.toDual b

Alias of the reverse direction of OrderDual.toDual_le_toDual.

theorem LT.lt.dual {α : Type u_1} [LT α] {a b : α} : b < a → OrderDual.toDual a < OrderDual.toDual b

Alias of the reverse direction of OrderDual.toDual_lt_toDual.

theorem LE.le.ofDual {α : Type u_1} [LE α] {a b : αᵒᵈ} : b ≤ a → OrderDual.ofDual a ≤ OrderDual.ofDual b

Alias of the reverse direction of OrderDual.ofDual_le_ofDual.

theorem LT.lt.ofDual {α : Type u_1} [LT α] {a b : αᵒᵈ} : b < a → OrderDual.ofDual a < OrderDual.ofDual b

Alias of the reverse direction of OrderDual.ofDual_lt_ofDual.

DenselyOrdered for OrderDual

instance OrderDual.denselyOrdered (α : Type u_2) [LT α] [h : DenselyOrdered α] : DenselyOrdered αᵒᵈ

@[simp]

theorem denselyOrdered_orderDual {α : Type u_1} [LT α] : DenselyOrdered αᵒᵈ ↔ DenselyOrdered α