@[irreducible]

def LE.opposite {α : Type u_1} (le : LE α) : LE α

Inverts an {name}LE instance.

The result is an {lean}LE α instance where {lit}a ≤ b holds when {name}le would have {lit}b ≤ a hold.

If {name}le obeys laws, then {lean}le.opposite obeys the opposite laws. For example, if {name}le encodes a linear order, then {lean}le.opposite also encodes a linear order. To automatically derive these laws, use {lit}open Std.OppositeOrderInstances.

For example, {name}LE.opposite can be used to derive maximum operations from minimum operations, since finding the minimum in the opposite order is the same as finding the maximum in the original order:

def min' [LE α] [DecidableLE α] (a b : α) : α :=
  if a ≤ b then a else b

open scoped Std.OppositeOrderInstances in
def max' [LE α] [DecidableLE α] (a b : α) : α :=
  letI : LE α := (inferInstanceAs (LE α)).opposite
  -- `DecidableLE` for the opposite order is derived automatically via `OppositeOrderInstances`
  min' a b

Without the open scoped command, Lean would not find the required {lit}DecidableLE α instance for the opposite order.

Equations

• le.opposite = { le := fun (a b : α) => b ≤ a }

theorem LE.opposite_def {α : Type u_1} {le : LE α} : le.opposite = { le := fun (a b : α) => b ≤ a }

theorem LE.le_opposite_iff {α : Type u_1} {le : LE α} {a b : α} : a ≤ b ↔ b ≤ a

@[irreducible]

def LT.opposite {α : Type u_1} (lt : LT α) : LT α

Inverts an {name}LT instance.

The result is an {lean}LT α instance where {lit}a < b holds when {name}lt would have {lit}b < a hold.

If {name}lt obeys laws, then {lean}lt.opposite obeys the opposite laws. To automatically derive these laws, use {lit}open scoped Std.OppositeOrderInstances.

For example, one can use the derived instances to prove properties about the opposite {name}LT instance:

open scoped Std.OppositeOrderInstances in
example [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsLinearOrder α] {x y : α} :
    letI : LE α := LE.opposite inferInstance
    letI : LT α := LT.opposite inferInstance
    ¬ y ≤ x ↔ x < y :=
  letI : LE α := LE.opposite inferInstance
  letI : LT α := LT.opposite inferInstance
  Std.not_le

Without the open scoped command, Lean would not find the {lit}LawfulOrderLT α and {lit}IsLinearOrder α instances for the opposite order that are required by {name}not_le.

Equations

• lt.opposite = { lt := fun (a b : α) => b < a }

theorem LT.opposite_def {α : Type u_1} {lt : LT α} : lt.opposite = { lt := fun (a b : α) => b < a }

theorem LT.lt_opposite_iff {α : Type u_1} {lt : LT α} {a b : α} : a < b ↔ b < a

@[irreducible]

def Min.oppositeMax {α : Type u_1} (min : Min α) : Max α

Creates a {name}Max instance from a {name}Min instance.

The result is a {lean}Max α instance that uses {lean}min.min as its {name}max operation.

If {name}min obeys laws, then {lean}min.oppositeMax obeys the corresponding laws for {name}Max. To automatically derive these laws, use {lit}open scoped Std.OppositeOrderInstances.

For example, one can use the derived instances to prove properties about the opposite {name}Max instance:

open scoped Std.OppositeOrderInstances in
example [LE α] [DecidableLE α] [Min α] [Std.LawfulOrderLeftLeaningMin α] {a b : α} :
    letI : LE α := LE.opposite inferInstance
    letI : Max α := (inferInstance : Min α).oppositeMax
    max a b = if b ≤ a then a else b :=
  letI : LE α := LE.opposite inferInstance
  letI : Max α := (inferInstance : Min α).oppositeMax
  Std.max_eq_if

Without the open scoped command, Lean would not find the {lit}LawfulOrderLeftLeaningMax α instance for the opposite order that is required by {name}max_eq_if.

Equations

• min.oppositeMax = { max := fun (a b : α) => Min.min a b }

theorem Min.oppositeMax_def {α : Type u_1} {min : Min α} : min.oppositeMax = { max := Min.min }

theorem Min.max_oppositeMax {α : Type u_1} {min : Min α} {a b : α} : max a b = Min.min a b

@[irreducible]

def Max.oppositeMin {α : Type u_1} (max : Max α) : Min α

Creates a {name}Min instance from a {name}Max instance.

The result is a {lean}Min α instance that uses {lean}max.max as its {name}min operation.

If {name}max obeys laws, then {lean}max.oppositeMin obeys the corresponding laws for {name}Min. To automatically derive these laws, use {lit}open scoped Std.OppositeOrderInstances.

For example, one can use the derived instances to prove properties about the opposite {name}Min instance:

open scoped Std.OppositeOrderInstances in
example [LE α] [DecidableLE α] [Max α] [Std.LawfulOrderLeftLeaningMax α] {a b : α} :
    letI : LE α := LE.opposite inferInstance
    letI : Min α := (inferInstance : Max α).oppositeMin
    min a b = if a ≤ b then a else b :=
  letI : LE α := LE.opposite inferInstance
  letI : Min α := (inferInstance : Max α).oppositeMin
  Std.min_eq_if

Without the open scoped command, Lean would not find the {lit}LawfulOrderLeftLeaningMin α instance for the opposite order that is required by {name}min_eq_if.

Equations

• max.oppositeMin = { min := fun (a b : α) => Max.max a b }

theorem Max.oppositeMin_def {α : Type u_1} {min : Max α} : min.oppositeMin = { min := max }

theorem Max.min_oppositeMin {α : Type u_1} {max : Max α} {a b : α} : min a b = Max.max a b

@[implicit_reducible]

def Std.OppositeOrderInstances.instDecidableLEOpposite {α : Type u_1} {i : LE α} [id : DecidableLE α] : DecidableLE α

Equations

• Std.OppositeOrderInstances.instDecidableLEOpposite a b = id b a

@[implicit_reducible]

def Std.OppositeOrderInstances.instDecidableLTOpposite {α : Type u_1} {i : LT α} [id : DecidableLT α] : DecidableLT α

Equations

• Std.OppositeOrderInstances.instDecidableLTOpposite a b = id b a

theorem Std.OppositeOrderInstances.instLEReflOpposite {α : Type u_1} {i : LE α} [Refl fun (x1 x2 : α) => x1 ≤ x2] : Refl fun (x1 x2 : α) => x1 ≤ x2

theorem Std.OppositeOrderInstances.instLESymmOpposite {α : Type u_1} {i : LE α} [Symm fun (x1 x2 : α) => x1 ≤ x2] : Symm fun (x1 x2 : α) => x1 ≤ x2

theorem Std.OppositeOrderInstances.instLEAntisymmOpposite {α : Type u_1} {i : LE α} [Antisymm fun (x1 x2 : α) => x1 ≤ x2] : Antisymm fun (x1 x2 : α) => x1 ≤ x2

theorem Std.OppositeOrderInstances.instLEAsymmOpposite {α : Type u_1} {i : LE α} [Asymm fun (x1 x2 : α) => x1 ≤ x2] : Asymm fun (x1 x2 : α) => x1 ≤ x2

@[implicit_reducible]

def Std.OppositeOrderInstances.instLETransOpposite {α : Type u_1} {i : LE α} [Trans (fun (x1 x2 : α) => x1 ≤ x2) (fun (x1 x2 : α) => x1 ≤ x2) fun (x1 x2 : α) => x1 ≤ x2] : Trans (fun (x1 x2 : α) => x1 ≤ x2) (fun (x1 x2 : α) => x1 ≤ x2) fun (x1 x2 : α) => x1 ≤ x2

Equations

• Std.OppositeOrderInstances.instLETransOpposite = { trans := ⋯ }

theorem Std.OppositeOrderInstances.instLETotalOpposite {α : Type u_1} {i : LE α} [Total fun (x1 x2 : α) => x1 ≤ x2] : Total fun (x1 x2 : α) => x1 ≤ x2

theorem Std.OppositeOrderInstances.instLEIrreflOpposite {α : Type u_1} {i : LE α} [Irrefl fun (x1 x2 : α) => x1 ≤ x2] : Irrefl fun (x1 x2 : α) => x1 ≤ x2

theorem Std.OppositeOrderInstances.instIsPreorderOpposite {α : Type u_1} {i : LE α} [IsPreorder α] : IsPreorder α

theorem Std.OppositeOrderInstances.instIsPartialOrderOpposite {α : Type u_1} {i : LE α} [IsPartialOrder α] : IsPartialOrder α

theorem Std.OppositeOrderInstances.instIsLinearPreorderOpposite {α : Type u_1} {i : LE α} [IsLinearPreorder α] : IsLinearPreorder α

theorem Std.OppositeOrderInstances.instIsLinearOrderOpposite {α : Type u_1} {i : LE α} [IsLinearOrder α] : IsLinearOrder α

theorem Std.OppositeOrderInstances.instLawfulOrderOrdOpposite {α : Type u_1} {il : LE α} {io : Ord α} [LawfulOrderOrd α] : LawfulOrderOrd α

theorem Std.OppositeOrderInstances.instLawfulOrderLTOpposite {α : Type u_1} {il : LE α} {it : LT α} [LawfulOrderLT α] : LawfulOrderLT α

theorem Std.OppositeOrderInstances.instLawfulOrderBEqOpposite {α : Type u_1} {il : LE α} {ib : BEq α} [LawfulOrderBEq α] : LawfulOrderBEq α

theorem Std.OppositeOrderInstances.instLawfulOrderInfOpposite {α : Type u_1} {il : LE α} {im : Min α} [LawfulOrderInf α] : LawfulOrderSup α

theorem Std.OppositeOrderInstances.instLawfulOrderMinOpposite {α : Type u_1} {il : LE α} {im : Min α} [LawfulOrderMin α] : LawfulOrderMax α

theorem Std.OppositeOrderInstances.instLawfulOrderSupOpposite {α : Type u_1} {il : LE α} {im : Max α} [LawfulOrderSup α] : LawfulOrderInf α

theorem Std.OppositeOrderInstances.instLawfulOrderMaxOpposite {α : Type u_1} {il : LE α} {im : Max α} [LawfulOrderMax α] : LawfulOrderMin α

theorem Std.OppositeOrderInstances.instLawfulOrderLeftLeaningMinOpposite {α : Type u_1} {il : LE α} {im : Min α} [LawfulOrderLeftLeaningMin α] : LawfulOrderLeftLeaningMax α

theorem Std.OppositeOrderInstances.instLawfulOrderLeftLeaningMaxOpposite {α : Type u_1} {il : LE α} {im : Max α} [LawfulOrderLeftLeaningMax α] : LawfulOrderLeftLeaningMin α