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 α.

Equations

• αᵒᵈ = α

def «term_ᵒᵈ» : Lean.TrailingParserDescr

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

Equations

• «term_ᵒᵈ» = Lean.ParserDescr.trailingNode `«term_ᵒᵈ» 1024 0 (Lean.ParserDescr.symbol "ᵒᵈ")

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) [LE α] : LE αᵒᵈ

Equations

• OrderDual.instLE α = { le := fun (x y : α) => y ≤ x }

@[implicit_reducible]

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

Equations

• OrderDual.instLT α = { lt := fun (x y : α) => y < x }

@[implicit_reducible]

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

Equations

• OrderDual.instOrd α = { compare := fun (a b : α) => compare b a }

@[implicit_reducible]

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

Equations

• OrderDual.instSup α = { max := fun (x1 x2 : α) => x1 ⊓ x2 }

@[implicit_reducible]

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

Equations

• OrderDual.instInf α = { min := fun (x1 x2 : α) => x1 ⊔ x2 }

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 αᵒᵈ

Equations

• OrderDual.instPreorder α = { toLE := OrderDual.instLE α, toLT := OrderDual.instLT α, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯ }

@[implicit_reducible]

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

Equations

• OrderDual.instPartialOrder α = { toPreorder := inferInstanceAs (Preorder αᵒᵈ), le_antisymm := ⋯ }

@[implicit_reducible]

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

Equations

• OrderDual.instDecidableEq α = inst✝

@[implicit_reducible]

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

Equations

• OrderDual.instDecidableLT α = inferInstanceAs (DecidableRel fun (a b : α) => b < a)

@[implicit_reducible]

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

Equations

• OrderDual.instDecidableLE α = inferInstanceAs (DecidableRel fun (a b : α) => b ≤ a)

@[implicit_reducible]

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

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

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

The opposite linear order to a given linear order

Equations

• LinearOrder.swap α x✝ = inferInstanceAs (LinearOrder αᵒᵈ)

@[implicit_reducible]

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

Equations

• OrderDual.instInhabited = x

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 αᵒᵈ

Equations

• OrderDual.instUnique = h

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

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

Equations

• OrderDual.toDual = Equiv.refl α

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

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

Equations

• OrderDual.ofDual = Equiv.refl αᵒᵈ

@[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 αᵒᵈ.

Equations

• OrderDual.rec toDual = toDual

@[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 α