Order instances on Shrink

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

noncomputable instance instBotShrink {α : Type u_1} [Small.{u, u_1} α] [Bot α] : Bot (Shrink.{u, u_1} α)

noncomputable instance instTopShrink {α : Type u_1} [Small.{u, u_1} α] [Top α] : Top (Shrink.{u, u_1} α)

@[simp]

theorem equivShrink_bot {α : Type u_1} [Small.{u, u_1} α] [Bot α] : (equivShrink α) ⊥ = ⊥

@[simp]

theorem equivShrink_top {α : Type u_1} [Small.{u, u_1} α] [Top α] : (equivShrink α) ⊤ = ⊤

@[simp]

theorem equivShrink_symm_bot {α : Type u_1} [Small.{u, u_1} α] [Bot α] : (equivShrink α).symm ⊥ = ⊥

@[simp]

theorem equivShrink_symm_top {α : Type u_1} [Small.{u, u_1} α] [Top α] : (equivShrink α).symm ⊤ = ⊤

instance instPreorderShrink {α : Type u_1} [Small.{u, u_1} α] [Preorder α] : Preorder (Shrink.{u, u_1} α)

noncomputable def orderIsoShrink (α : Type u_1) [Small.{u, u_1} α] [Preorder α] : α ≃o Shrink.{u, u_1} α

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

@[simp]

theorem orderIsoShrink_apply {α : Type u_1} [Small.{u, u_1} α] [Preorder α] (a : α) : (orderIsoShrink α) a = (equivShrink α) a

@[simp]

theorem orderIsoShrink_symm_apply {α : Type u_1} [Small.{u, u_1} α] [Preorder α] (a : Shrink.{u, u_1} α) : (orderIsoShrink α).symm a = (equivShrink α).symm a

@[simp]

theorem equivShrink_le_equivShrink {α : Type u_1} [Small.{u, u_1} α] [Preorder α] {x y : α} : (equivShrink α) x ≤ (equivShrink α) y ↔ x ≤ y

@[simp]

theorem equivShrink_lt_equivShrink {α : Type u_1} [Small.{u, u_1} α] [Preorder α] {x y : α} : (equivShrink α) x < (equivShrink α) y ↔ x < y

noncomputable instance instOrderBotShrink {α : Type u_1} [Small.{u, u_1} α] [Preorder α] [OrderBot α] : OrderBot (Shrink.{u, u_1} α)

noncomputable instance instOrderTopShrink {α : Type u_1} [Small.{u, u_1} α] [Preorder α] [OrderTop α] : OrderTop (Shrink.{u, u_1} α)

noncomputable instance instSuccOrderShrink {α : Type u_1} [Small.{u, u_1} α] [Preorder α] [SuccOrder α] : SuccOrder (Shrink.{u, u_1} α)

noncomputable instance instPredOrderShrink {α : Type u_1} [Small.{u, u_1} α] [Preorder α] [PredOrder α] : PredOrder (Shrink.{u, u_1} α)

instance instWellFoundedLTShrink {α : Type u_1} [Small.{u, u_1} α] [Preorder α] [WellFoundedLT α] : WellFoundedLT (Shrink.{u, u_1} α)

instance instWellFoundedGTShrink {α : Type u_1} [Small.{u, u_1} α] [Preorder α] [WellFoundedGT α] : WellFoundedGT (Shrink.{u, u_1} α)

instance instPartialOrderShrink {α : Type u_1} [Small.{u, u_1} α] [PartialOrder α] : PartialOrder (Shrink.{u, u_1} α)

noncomputable instance instLinearOrderShrink {α : Type u_1} [Small.{u, u_1} α] [LinearOrder α] : LinearOrder (Shrink.{u, u_1} α)