Documentation

Mathlib.Order.OrderDual

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:

source
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
    Instances For
      source
      def «term_ᵒᵈ» :
      Lean.TrailingParserDescr

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

      Equations
        Instances For
          source
          instance OrderDual.instNonempty (α : Type u_2) [h : Nonempty α] :
          Nonempty αᵒᵈ
          source
          instance OrderDual.instSubsingleton (α : Type u_2) [h : Subsingleton α] :
          Subsingleton αᵒᵈ
          source
          instance OrderDual.instLE (α : Type u_2) [LE α] :
          LE αᵒᵈ
          Equations
            source
            instance OrderDual.instLT (α : Type u_2) [LT α] :
            LT αᵒᵈ
            Equations
              source
              instance OrderDual.instOrd (α : Type u_2) [Ord α] :
              Ord αᵒᵈ
              Equations
                source
                instance OrderDual.instSup (α : Type u_2) [Min α] :
                Max αᵒᵈ
                Equations
                  source
                  instance OrderDual.instInf (α : Type u_2) [Max α] :
                  Min αᵒᵈ
                  Equations
                    source
                    instance OrderDual.instIsTransLE {α : Type u_1} [LE α] [T : IsTrans α LE.le] :
                    IsTrans αᵒᵈ LE.le
                    source
                    instance OrderDual.instIsTransLT {α : Type u_1} [LT α] [T : IsTrans α LT.lt] :
                    IsTrans αᵒᵈ LT.lt
                    source
                    instance OrderDual.instTrichotomousLt {α : Type u_1} [LT α] [T : Std.Trichotomous LT.lt] :
                    Std.Trichotomous LT.lt
                    source
                    instance OrderDual.instPreorder (α : Type u_2) [Preorder α] :
                    Preorder αᵒᵈ
                    Equations
                      source
                      instance OrderDual.instPartialOrder (α : Type u_2) [PartialOrder α] :
                      PartialOrder αᵒᵈ
                      Equations
                        source
                        instance OrderDual.instDecidableEq (α : Type u_2) [DecidableEq α] :
                        DecidableEq αᵒᵈ
                        Equations
                          source
                          instance OrderDual.instDecidableLT (α : Type u_2) [LT α] [DecidableLT α] :
                          DecidableLT αᵒᵈ
                          Equations
                            source
                            instance OrderDual.instDecidableLE (α : Type u_2) [LE α] [DecidableLE α] :
                            DecidableLE αᵒᵈ
                            Equations
                              source
                              instance OrderDual.instLinearOrder (α : Type u_2) [LinearOrder α] :
                              LinearOrder αᵒᵈ
                              Equations
                                source
                                def LinearOrder.swap (α : Type u_2) :
                                LinearOrder α → LinearOrder α

                                The opposite linear order to a given linear order

                                Equations
                                  Instances For
                                    source
                                    instance OrderDual.instInhabited {α : Type u_1} [Inhabited α] :
                                    Inhabited αᵒᵈ
                                    Equations
                                      source
                                      theorem OrderDual.Ord.dual_dual (α : Type u_2) [H : Ord α] :
                                      instOrd αᵒᵈ = H
                                      source
                                      theorem OrderDual.Preorder.dual_dual (α : Type u_2) [H : Preorder α] :
                                      instPreorder αᵒᵈ = H
                                      source
                                      theorem OrderDual.instPartialOrder.dual_dual (α : Type u_2) [H : PartialOrder α] :
                                      instPartialOrder αᵒᵈ = H
                                      source
                                      theorem OrderDual.instLinearOrder.dual_dual (α : Type u_2) [H : LinearOrder α] :
                                      instLinearOrder αᵒᵈ = H

                                      DenselyOrdered for OrderDual #

                                      source
                                      instance OrderDual.denselyOrdered (α : Type u_2) [LT α] [h : DenselyOrdered α] :
                                      DenselyOrdered αᵒᵈ
                                      source
                                      @[simp]
                                      theorem denselyOrdered_orderDual {α : Type u_1} [LT α] :
                                      DenselyOrdered αᵒᵈ ↔ DenselyOrdered α