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

Equations

• OrderDual.instLE α = { le := fun (a b : αᵒᵈ) => b ≤ a }

@[implicit_reducible]

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

Equations

• OrderDual.instLT α = { lt := fun (a b : αᵒᵈ) => b < a }

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

• OrderDual.instMaxOfMin α = { max := fun (a b : αᵒᵈ) => a ⊓ b }

@[implicit_reducible]

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

Equations

• OrderDual.instMinOfMax α = { min := fun (a b : αᵒᵈ) => a ⊔ b }

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 := OrderDual.instPreorder α, 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 α] [h : DecidableLT α] : DecidableLT αᵒᵈ

Equations

• OrderDual.instDecidableLT α a b = h b a

@[implicit_reducible]

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

Equations

• OrderDual.instDecidableLE α a b = h 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, deprecated "This declaration shouldn't have existed" (since := "2026-04-08")]

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

The opposite linear order to a given linear order

Equations

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

@[implicit_reducible]

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

Equations

• OrderDual.instInhabited = { default := default }

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 = { toInhabited := OrderDual.instInhabited, uniq := ⋯ }

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 α

Pushing order definitions through Equiv

@[reducible, inline]

abbrev Equiv.top {α : Type u_1} {β : Type u_2} (e : α ≃ β) [Top β] : Top α

Transfer Top across an Equiv.

Equations

• e.top = { top := e.symm ⊤ }

theorem Equiv.top_def {α : Type u_1} {β : Type u_2} (e : α ≃ β) [Top β] : ⊤ = e.symm ⊤

@[reducible, inline]

abbrev Equiv.bot {α : Type u_1} {β : Type u_2} (e : α ≃ β) [Bot β] : Bot α

Transfer Bot across an Equiv.

Equations

• e.bot = { bot := e.symm ⊥ }

theorem Equiv.bot_def {α : Type u_1} {β : Type u_2} (e : α ≃ β) [Bot β] : ⊥ = e.symm ⊥

@[reducible, inline]

abbrev Equiv.compl {α : Type u_1} {β : Type u_2} (e : α ≃ β) [Compl β] : Compl α

Transfer Compl across an Equiv.

Equations

• e.compl = { compl := fun (a : α) => e.symm (e a)ᶜ }

theorem Equiv.compl_def {α : Type u_1} {β : Type u_2} (e : α ≃ β) [Compl β] (a : α) : aᶜ = e.symm (e a)ᶜ

@[reducible, inline]

abbrev Equiv.sdiff {α : Type u_1} {β : Type u_2} (e : α ≃ β) [SDiff β] : SDiff α

Transfer SDiff across an Equiv.

Equations

• e.sdiff = { sdiff := fun (a b : α) => e.symm (e a \ e b) }

theorem Equiv.sdiff_def {α : Type u_1} {β : Type u_2} (e : α ≃ β) [SDiff β] (a b : α) : a \ b = e.symm (e a \ e b)

@[reducible, inline]

abbrev Equiv.himp {α : Type u_1} {β : Type u_2} (e : α ≃ β) [HImp β] : HImp α

Transfer HImp across an Equiv.

Equations

• e.himp = { himp := fun (a b : α) => e.symm (e a ⇨ e b) }

theorem Equiv.himp_def {α : Type u_1} {β : Type u_2} (e : α ≃ β) [HImp β] (a b : α) : a ⇨ b = e.symm (e a ⇨ e b)

@[reducible, inline]

abbrev Equiv.hnot {α : Type u_1} {β : Type u_2} (e : α ≃ β) [HNot β] : HNot α

Transfer HNot across an Equiv.

Equations

• e.hnot = { hnot := fun (a : α) => e.symm (￢e a) }

theorem Equiv.hnot_def {α : Type u_1} {β : Type u_2} (e : α ≃ β) [HNot β] (a : α) : ￢a = e.symm (￢e a)