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} α)

Equations

• instBotShrink = { bot := (equivShrink α) ⊥ }

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

Equations

• instTopShrink = { top := (equivShrink α) ⊤ }

@[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} α)

Equations

• instPreorderShrink = Preorder.lift ⇑(equivShrink α).symm

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

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

Equations

• orderIsoShrink α = { toEquiv := equivShrink α, map_rel_iff' := ⋯ }

@[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} α)

Equations

• instOrderBotShrink = { toBot := instBotShrink, bot_le := ⋯ }

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

Equations

• instOrderTopShrink = { toTop := instTopShrink, le_top := ⋯ }

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

Equations

• instSuccOrderShrink = SuccOrder.ofOrderIso (orderIsoShrink α)

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

Equations

• instPredOrderShrink = PredOrder.ofOrderIso (orderIsoShrink α)

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} α)

Equations

• instPartialOrderShrink = Function.Injective.partialOrder ⇑(equivShrink α).symm ⋯ ⋯ ⋯

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

Equations

• instLinearOrderShrink = LinearOrder.lift' ⇑(equivShrink α).symm ⋯