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
noncomputable instance instBotShrink {α : Type u_1} [Small.{u, u_1} α] [Bot α] :
Bot (Shrink.{u, u_1} α)
Equations
    source
    noncomputable instance instTopShrink {α : Type u_1} [Small.{u, u_1} α] [Top α] :
    Top (Shrink.{u, u_1} α)
    Equations
      source
      @[simp]
      theorem equivShrink_bot {α : Type u_1} [Small.{u, u_1} α] [Bot α] :
      (equivShrink α) ⊥ = ⊥
      source
      @[simp]
      theorem equivShrink_top {α : Type u_1} [Small.{u, u_1} α] [Top α] :
      (equivShrink α) ⊤ = ⊤
      source
      @[simp]
      theorem equivShrink_symm_bot {α : Type u_1} [Small.{u, u_1} α] [Bot α] :
      (equivShrink α).symm ⊥ = ⊥
      source
      @[simp]
      theorem equivShrink_symm_top {α : Type u_1} [Small.{u, u_1} α] [Top α] :
      (equivShrink α).symm ⊤ = ⊤
      source
      instance instPreorderShrink {α : Type u_1} [Small.{u, u_1} α] [Preorder α] :
      Preorder (Shrink.{u, u_1} α)
      Equations
        source
        noncomputable def orderIsoShrink (α : Type u_1) [Small.{u, u_1} α] [Preorder α] :
        α ≃o Shrink.{u, u_1} α

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

        Equations
          Instances For
            source
            @[simp]
            theorem orderIsoShrink_apply {α : Type u_1} [Small.{u, u_1} α] [Preorder α] (a : α) :
            (orderIsoShrink α) a = (equivShrink α) a
            source
            @[simp]
            theorem orderIsoShrink_symm_apply {α : Type u_1} [Small.{u, u_1} α] [Preorder α] (a : Shrink.{u, u_1} α) :
            (orderIsoShrink α).symm a = (equivShrink α).symm a
            source
            @[simp]
            theorem equivShrink_le_equivShrink {α : Type u_1} [Small.{u, u_1} α] [Preorder α] {x y : α} :
            (equivShrink α) x ≤ (equivShrink α) y ↔ x ≤ y
            source
            @[simp]
            theorem equivShrink_lt_equivShrink {α : Type u_1} [Small.{u, u_1} α] [Preorder α] {x y : α} :
            (equivShrink α) x < (equivShrink α) y ↔ x < y
            source
            noncomputable instance instOrderBotShrink {α : Type u_1} [Small.{u, u_1} α] [Preorder α] [OrderBot α] :
            OrderBot (Shrink.{u, u_1} α)
            Equations
              source
              noncomputable instance instOrderTopShrink {α : Type u_1} [Small.{u, u_1} α] [Preorder α] [OrderTop α] :
              OrderTop (Shrink.{u, u_1} α)
              Equations
                source
                noncomputable instance instSuccOrderShrink {α : Type u_1} [Small.{u, u_1} α] [Preorder α] [SuccOrder α] :
                SuccOrder (Shrink.{u, u_1} α)
                Equations
                  source
                  noncomputable instance instPredOrderShrink {α : Type u_1} [Small.{u, u_1} α] [Preorder α] [PredOrder α] :
                  PredOrder (Shrink.{u, u_1} α)
                  Equations
                    source
                    instance instWellFoundedLTShrink {α : Type u_1} [Small.{u, u_1} α] [Preorder α] [WellFoundedLT α] :
                    WellFoundedLT (Shrink.{u, u_1} α)
                    source
                    instance instWellFoundedGTShrink {α : Type u_1} [Small.{u, u_1} α] [Preorder α] [WellFoundedGT α] :
                    WellFoundedGT (Shrink.{u, u_1} α)
                    source
                    instance instPartialOrderShrink {α : Type u_1} [Small.{u, u_1} α] [PartialOrder α] :
                    PartialOrder (Shrink.{u, u_1} α)
                    Equations
                      source
                      noncomputable instance instLinearOrderShrink {α : Type u_1} [Small.{u, u_1} α] [LinearOrder α] :
                      LinearOrder (Shrink.{u, u_1} α)
                      Equations