Documentation

Mathlib.Order.Shrink

Order instances on Shrink #

If α : Type v is u-small, we transport various order related instances on α to Shrink.{u} α.

source
instance instPreorderShrink (α : Type v) [Small.{u, v} α] [Preorder α] :
Preorder (Shrink.{u, v} α)
Equations
    source
    noncomputable def orderIsoShrink (α : Type v) [Small.{u, v} α] [Preorder α] :
    α ≃o Shrink.{u, v} α

    The order isomorphism α ≃o Shrink.{u} α.

    Equations
      Instances For
        source
        @[simp]
        theorem orderIsoShrink_apply {α : Type v} [Small.{u, v} α] [Preorder α] (a : α) :
        (orderIsoShrink α) a = (equivShrink α) a
        source
        @[simp]
        theorem orderIsoShrink_symm_apply {α : Type v} [Small.{u, v} α] [Preorder α] (a : Shrink.{u, v} α) :
        (orderIsoShrink α).symm a = (equivShrink α).symm a
        source
        instance instPartialOrderShrink {α : Type v} [Small.{u, v} α] [PartialOrder α] :
        PartialOrder (Shrink.{u, v} α)
        Equations
          source
          noncomputable instance instLinearOrderShrink {α : Type v} [Small.{u, v} α] [LinearOrder α] :
          LinearOrder (Shrink.{u, v} α)
          Equations
            source
            noncomputable instance instBotShrink {α : Type v} [Small.{u, v} α] [Bot α] :
            Bot (Shrink.{u, v} α)
            Equations
              source
              @[simp]
              theorem equivShrink_bot {α : Type v} [Small.{u, v} α] [Bot α] :
              (equivShrink α) ⊥ = ⊥
              source
              @[simp]
              theorem equivShrink_symm_bot {α : Type v} [Small.{u, v} α] [Bot α] :
              (equivShrink α).symm ⊥ = ⊥
              source
              noncomputable instance instTopShrink {α : Type v} [Small.{u, v} α] [Top α] :
              Top (Shrink.{u, v} α)
              Equations
                source
                @[simp]
                theorem equivShrink_top {α : Type v} [Small.{u, v} α] [Top α] :
                (equivShrink α) ⊤ = ⊤
                source
                @[simp]
                theorem equivShrink_symm_top {α : Type v} [Small.{u, v} α] [Top α] :
                (equivShrink α).symm ⊤ = ⊤
                source
                noncomputable instance instOrderBotShrink {α : Type v} [Small.{u, v} α] [Preorder α] [OrderBot α] :
                OrderBot (Shrink.{u, v} α)
                Equations
                  source
                  noncomputable instance instOrderTopShrink {α : Type v} [Small.{u, v} α] [Preorder α] [OrderTop α] :
                  OrderTop (Shrink.{u, v} α)
                  Equations
                    source
                    noncomputable instance instSuccOrderShrink {α : Type v} [Small.{u, v} α] [Preorder α] [SuccOrder α] :
                    SuccOrder (Shrink.{u, v} α)
                    Equations
                      source
                      noncomputable instance instPredOrderShrink {α : Type v} [Small.{u, v} α] [Preorder α] [PredOrder α] :
                      PredOrder (Shrink.{u, v} α)
                      Equations
                        source
                        instance instWellFoundedLTShrink {α : Type v} [Small.{u, v} α] [Preorder α] [WellFoundedLT α] :
                        WellFoundedLT (Shrink.{u, v} α)