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
@[instance_reducible]
noncomputable instance instBotShrink {α : Type u_1} [Small.{u, u_1} α] [Bot α] :
Bot (Shrink.{u, u_1} α)
source
@[instance_reducible]
noncomputable instance instTopShrink {α : Type u_1} [Small.{u, u_1} α] [Top α] :
Top (Shrink.{u, u_1} α)
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_reducible]
noncomputable instance instPreorderShrink {α : Type u_1} [Small.{u, u_1} α] [Preorder α] :
Preorder (Shrink.{u, u_1} α)
source
noncomputable def orderIsoShrink (α : Type u_1) [Small.{u, u_1} α] [Preorder α] :
α ≃o Shrink.{u, u_1} α

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

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
    @[instance_reducible]
    noncomputable instance instOrderBotShrink {α : Type u_1} [Small.{u, u_1} α] [Preorder α] [OrderBot α] :
    OrderBot (Shrink.{u, u_1} α)
    source
    @[instance_reducible]
    noncomputable instance instOrderTopShrink {α : Type u_1} [Small.{u, u_1} α] [Preorder α] [OrderTop α] :
    OrderTop (Shrink.{u, u_1} α)
    source
    @[instance_reducible]
    noncomputable instance instSuccOrderShrink {α : Type u_1} [Small.{u, u_1} α] [Preorder α] [SuccOrder α] :
    SuccOrder (Shrink.{u, u_1} α)
    source
    @[instance_reducible]
    noncomputable instance instPredOrderShrink {α : Type u_1} [Small.{u, u_1} α] [Preorder α] [PredOrder α] :
    PredOrder (Shrink.{u, u_1} α)
    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_reducible]
    noncomputable instance instPartialOrderShrink {α : Type u_1} [Small.{u, u_1} α] [PartialOrder α] :
    PartialOrder (Shrink.{u, u_1} α)
    source
    @[instance_reducible]
    noncomputable instance instLinearOrderShrink {α : Type u_1} [Small.{u, u_1} α] [LinearOrder α] :
    LinearOrder (Shrink.{u, u_1} α)