Order instances on Shrink

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

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

Equations

• instPreorderShrink α = { le := fun (a b : Shrink.{?u.20, ?u.19} α) => (equivShrink α).symm a ≤ (equivShrink α).symm b, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_le := ⋯ }

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

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

Equations

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

@[simp]

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

@[simp]

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

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

Equations

• instPartialOrderShrink = { toPreorder := instPreorderShrink α, le_antisymm := ⋯ }

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

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

@[simp]

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

@[simp]

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

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

Equations

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

@[simp]

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

@[simp]

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

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

Equations

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

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

Equations

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

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

Equations

• instSuccOrderShrink = SuccOrder.ofOrderIso (orderIsoShrink α)

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

Equations

• instPredOrderShrink = PredOrder.ofOrderIso (orderIsoShrink α)

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