Order instances on Shrink #
If α : Type v
is u
-small, we transport various order related
instances on α
to Shrink.{u} α
.
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 := ⋯ }
The order isomorphism α ≃o Shrink.{u} α
.
Equations
- orderIsoShrink α = { toEquiv := equivShrink α, map_rel_iff' := ⋯ }
Instances For
@[simp]
@[simp]
theorem
orderIsoShrink_symm_apply
{α : Type v}
[Small.{u, v} α]
[Preorder α]
(a : Shrink.{u, v} α)
:
Equations
- instPartialOrderShrink = { toPreorder := instPreorderShrink α, le_antisymm := ⋯ }
Equations
- One or more equations did not get rendered due to their size.
Equations
- instBotShrink = { bot := (equivShrink α) ⊥ }
@[simp]
Equations
- instTopShrink = { top := (equivShrink α) ⊤ }
@[simp]
Equations
- instOrderBotShrink = { toBot := instBotShrink, bot_le := ⋯ }
Equations
- instOrderTopShrink = { toTop := instTopShrink, le_top := ⋯ }
noncomputable instance
instSuccOrderShrink
{α : Type v}
[Small.{u, v} α]
[Preorder α]
[SuccOrder α]
:
Equations
noncomputable instance
instPredOrderShrink
{α : Type v}
[Small.{u, v} α]
[Preorder α]
[PredOrder α]
: