Documentation

Mathlib.Order.Hom.Bounded

Bounded order homomorphisms #

This file defines (bounded) order homomorphisms.

We use the FunLike design, so each type of morphisms has a companion typeclass which is meant to be satisfied by itself and all stricter types.

Types of morphisms #

Typeclasses #

structure TopHom (α : Type u_1) (β : Type u_2) [inst : Top α] [inst : Top β] :
Type (maxu_1u_2)
  • The underlying function. The preferred spelling is FunLike.coe.

    toFun : αβ
  • The function preserves the top element. The preferred spelling is map_top.

    map_top' : toFun =

The type of ⊤⊤-preserving functions from α to β.

Instances For
    structure BotHom (α : Type u_1) (β : Type u_2) [inst : Bot α] [inst : Bot β] :
    Type (maxu_1u_2)
    • The underlying function. The preferred spelling is FunLike.coe.

      toFun : αβ
    • The function preserves the bottom element. The preferred spelling is map_bot.

      map_bot' : toFun =

    The type of ⊥⊥-preserving functions from α to β.

    Instances For
      structure BoundedOrderHom (α : Type u_1) (β : Type u_2) [inst : Preorder α] [inst : Preorder β] [inst : BoundedOrder α] [inst : BoundedOrder β] extends OrderHom :
      Type (maxu_1u_2)
      • The function preserves the top element. The preferred spelling is map_top.

        map_top' : toOrderHom =
      • The function preserves the bottom element. The preferred spelling is map_bot.

        map_bot' : toOrderHom =

      The type of bounded order homomorphisms from α to β.

      Instances For
        class TopHomClass (F : Type u_1) (α : outParam (Type u_2)) (β : outParam (Type u_3)) [inst : Top α] [inst : Top β] extends FunLike :
        Type (max(maxu_1u_2)u_3)

        TopHomClass F α β states that F is a type of ⊤⊤-preserving morphisms.

        You should extend this class when you extend TopHom.

        Instances
          class BotHomClass (F : Type u_1) (α : outParam (Type u_2)) (β : outParam (Type u_3)) [inst : Bot α] [inst : Bot β] extends FunLike :
          Type (max(maxu_1u_2)u_3)

          BotHomClass F α β states that F is a type of ⊥⊥-preserving morphisms.

          You should extend this class when you extend BotHom.

          Instances
            class BoundedOrderHomClass (F : Type u_1) (α : outParam (Type u_2)) (β : outParam (Type u_3)) [inst : LE α] [inst : LE β] [inst : BoundedOrder α] [inst : BoundedOrder β] extends RelHomClass :
            Type (max(maxu_1u_2)u_3)
            • Morphisms preserve the top element. The preferred spelling is _root_.map_top.

              map_top : ∀ (f : F), f =
            • Morphisms preserve the bottom element. The preferred spelling is _root_.map_bot.

              map_bot : ∀ (f : F), f =

            BoundedOrderHomClass F α β states that F is a type of bounded order morphisms.

            You should extend this class when you extend BoundedOrderHom.

            Instances
              instance BoundedOrderHomClass.toTopHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} :
              {x : LE α} → {x_1 : LE β} → {x_2 : BoundedOrder α} → {x_3 : BoundedOrder β} → [inst : BoundedOrderHomClass F α β] → TopHomClass F α β
              Equations
              instance BoundedOrderHomClass.toBotHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} :
              {x : LE α} → {x_1 : LE β} → {x_2 : BoundedOrder α} → {x_3 : BoundedOrder β} → [inst : BoundedOrderHomClass F α β] → BotHomClass F α β
              Equations
              instance OrderIsoClass.toTopHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} :
              {x : LE α} → {x_1 : OrderTop α} → {x_2 : PartialOrder β} → {x_3 : OrderTop β} → [inst : OrderIsoClass F α β] → TopHomClass F α β
              Equations
              • OrderIsoClass.toTopHomClass = let src := let_fun this := inferInstance; this; TopHomClass.mk (_ : ∀ (f : F), f = )
              instance OrderIsoClass.toBotHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} :
              {x : LE α} → {x_1 : OrderBot α} → {x_2 : PartialOrder β} → {x_3 : OrderBot β} → [inst : OrderIsoClass F α β] → BotHomClass F α β
              Equations
              • OrderIsoClass.toBotHomClass = let src := let_fun this := inferInstance; this; BotHomClass.mk (_ : ∀ (f : F), f = )
              instance OrderIsoClass.toBoundedOrderHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} :
              {x : LE α} → {x_1 : BoundedOrder α} → {x_2 : PartialOrder β} → {x_3 : BoundedOrder β} → [inst : OrderIsoClass F α β] → BoundedOrderHomClass F α β
              Equations
              • One or more equations did not get rendered due to their size.
              @[simp]
              theorem map_eq_top_iff {F : Type u_3} {α : Type u_1} {β : Type u_2} [inst : LE α] [inst : OrderTop α] [inst : PartialOrder β] [inst : OrderTop β] [inst : OrderIsoClass F α β] (f : F) {a : α} :
              f a = a =
              @[simp]
              theorem map_eq_bot_iff {F : Type u_3} {α : Type u_1} {β : Type u_2} [inst : LE α] [inst : OrderBot α] [inst : PartialOrder β] [inst : OrderBot β] [inst : OrderIsoClass F α β] (f : F) {a : α} :
              f a = a =
              def TopHomClass.toTopHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Top α] [inst : Top β] [inst : TopHomClass F α β] (f : F) :
              TopHom α β

              Turn an element of a type F satisfying TopHomClass F α β into an actual TopHom. This is declared as the default coercion from F to TopHom α β.

              Equations
              • f = { toFun := f, map_top' := (_ : f = ) }
              instance instCoeTCTopHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Top α] [inst : Top β] [inst : TopHomClass F α β] :
              CoeTC F (TopHom α β)
              Equations
              • instCoeTCTopHom = { coe := TopHomClass.toTopHom }
              def BotHomClass.toBotHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Bot α] [inst : Bot β] [inst : BotHomClass F α β] (f : F) :
              BotHom α β

              Turn an element of a type F satisfying BotHomClass F α β into an actual BotHom. This is declared as the default coercion from F to BotHom α β.

              Equations
              • f = { toFun := f, map_bot' := (_ : f = ) }
              instance instCoeTCBotHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Bot α] [inst : Bot β] [inst : BotHomClass F α β] :
              CoeTC F (BotHom α β)
              Equations
              • instCoeTCBotHom = { coe := BotHomClass.toBotHom }
              def BoundedOrderHomClass.toBoundedOrderHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst : Preorder β] [inst : BoundedOrder α] [inst : BoundedOrder β] [inst : BoundedOrderHomClass F α β] (f : F) :

              Turn an element of a type F satisfying BoundedOrderHomClass F α β into an actual BoundedOrderHom. This is declared as the default coercion from F to BoundedOrderHom α β.

              Equations
              • f = let src := f; { toOrderHom := { toFun := f, monotone' := (_ : Monotone src) }, map_top' := (_ : f = ), map_bot' := (_ : f = ) }
              instance instCoeTCBoundedOrderHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst : Preorder β] [inst : BoundedOrder α] [inst : BoundedOrder β] [inst : BoundedOrderHomClass F α β] :
              Equations
              • instCoeTCBoundedOrderHom = { coe := BoundedOrderHomClass.toBoundedOrderHom }

              Top homomorphisms #

              instance TopHom.instTopHomClassTopHom {α : Type u_1} {β : Type u_2} [inst : Top α] [inst : Top β] :
              TopHomClass (TopHom α β) α β
              Equations
              theorem TopHom.ext {α : Type u_1} {β : Type u_2} [inst : Top α] [inst : Top β] {f : TopHom α β} {g : TopHom α β} (h : ∀ (a : α), f a = g a) :
              f = g
              def TopHom.copy {α : Type u_1} {β : Type u_2} [inst : Top α] [inst : Top β] (f : TopHom α β) (f' : αβ) (h : f' = f) :
              TopHom α β

              Copy of a TopHom with a new toFun equal to the old one. Useful to fix definitional equalities.

              Equations
              @[simp]
              theorem TopHom.coe_copy {α : Type u_1} {β : Type u_2} [inst : Top α] [inst : Top β] (f : TopHom α β) (f' : αβ) (h : f' = f) :
              ↑(TopHom.copy f f' h) = f'
              theorem TopHom.copy_eq {α : Type u_1} {β : Type u_2} [inst : Top α] [inst : Top β] (f : TopHom α β) (f' : αβ) (h : f' = f) :
              TopHom.copy f f' h = f
              instance TopHom.instInhabitedTopHom {α : Type u_1} {β : Type u_2} [inst : Top α] [inst : Top β] :
              Equations
              • TopHom.instInhabitedTopHom = { default := { toFun := fun x => , map_top' := (_ : (fun x => ) = (fun x => ) ) } }
              def TopHom.id (α : Type u_1) [inst : Top α] :
              TopHom α α

              id as a TopHom.

              Equations
              @[simp]
              theorem TopHom.coe_id (α : Type u_1) [inst : Top α] :
              ↑(TopHom.id α) = id
              @[simp]
              theorem TopHom.id_apply {α : Type u_1} [inst : Top α] (a : α) :
              ↑(TopHom.id α) a = a
              def TopHom.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Top α] [inst : Top β] [inst : Top γ] (f : TopHom β γ) (g : TopHom α β) :
              TopHom α γ

              Composition of TopHoms as a TopHom.

              Equations
              @[simp]
              theorem TopHom.coe_comp {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : Top α] [inst : Top β] [inst : Top γ] (f : TopHom β γ) (g : TopHom α β) :
              ↑(TopHom.comp f g) = f g
              @[simp]
              theorem TopHom.comp_apply {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : Top α] [inst : Top β] [inst : Top γ] (f : TopHom β γ) (g : TopHom α β) (a : α) :
              ↑(TopHom.comp f g) a = f (g a)
              @[simp]
              theorem TopHom.comp_assoc {α : Type u_4} {β : Type u_3} {γ : Type u_1} {δ : Type u_2} [inst : Top α] [inst : Top β] [inst : Top γ] [inst : Top δ] (f : TopHom γ δ) (g : TopHom β γ) (h : TopHom α β) :
              @[simp]
              theorem TopHom.comp_id {α : Type u_1} {β : Type u_2} [inst : Top α] [inst : Top β] (f : TopHom α β) :
              @[simp]
              theorem TopHom.id_comp {α : Type u_1} {β : Type u_2} [inst : Top α] [inst : Top β] (f : TopHom α β) :
              theorem TopHom.cancel_right {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : Top α] [inst : Top β] [inst : Top γ] {g₁ : TopHom β γ} {g₂ : TopHom β γ} {f : TopHom α β} (hf : Function.Surjective f) :
              TopHom.comp g₁ f = TopHom.comp g₂ f g₁ = g₂
              theorem TopHom.cancel_left {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : Top α] [inst : Top β] [inst : Top γ] {g : TopHom β γ} {f₁ : TopHom α β} {f₂ : TopHom α β} (hg : Function.Injective g) :
              TopHom.comp g f₁ = TopHom.comp g f₂ f₁ = f₂
              instance TopHom.instPreorderTopHom {α : Type u_1} {β : Type u_2} [inst : Top α] [inst : Preorder β] [inst : Top β] :
              Equations
              instance TopHom.instPartialOrderTopHom {α : Type u_1} {β : Type u_2} [inst : Top α] [inst : PartialOrder β] [inst : Top β] :
              Equations
              instance TopHom.instOrderTopTopHomToTopToLEToLEInstPreorderTopHom {α : Type u_1} {β : Type u_2} [inst : Top α] [inst : Preorder β] [inst : OrderTop β] :
              Equations
              • TopHom.instOrderTopTopHomToTopToLEToLEInstPreorderTopHom = OrderTop.mk (_ : ∀ (x : TopHom α β), (fun i => x i) )
              @[simp]
              theorem TopHom.coe_top {α : Type u_1} {β : Type u_2} [inst : Top α] [inst : Preorder β] [inst : OrderTop β] :
              =
              @[simp]
              theorem TopHom.top_apply {α : Type u_2} {β : Type u_1} [inst : Top α] [inst : Preorder β] [inst : OrderTop β] (a : α) :
              a =
              instance TopHom.instInfTopHomToTopToLEToPreorderToPartialOrder {α : Type u_1} {β : Type u_2} [inst : Top α] [inst : SemilatticeInf β] [inst : OrderTop β] :
              Inf (TopHom α β)
              Equations
              • TopHom.instInfTopHomToTopToLEToPreorderToPartialOrder = { inf := fun f g => { toFun := f g, map_top' := (_ : ((αβ) Pi.instInfForAll) f g = ) } }
              instance TopHom.instSemilatticeInfTopHomToTopToLEToPreorderToPartialOrder {α : Type u_1} {β : Type u_2} [inst : Top α] [inst : SemilatticeInf β] [inst : OrderTop β] :
              Equations
              • One or more equations did not get rendered due to their size.
              @[simp]
              theorem TopHom.coe_inf {α : Type u_1} {β : Type u_2} [inst : Top α] [inst : SemilatticeInf β] [inst : OrderTop β] (f : TopHom α β) (g : TopHom α β) :
              ↑(f g) = f g
              @[simp]
              theorem TopHom.inf_apply {α : Type u_2} {β : Type u_1} [inst : Top α] [inst : SemilatticeInf β] [inst : OrderTop β] (f : TopHom α β) (g : TopHom α β) (a : α) :
              ↑(f g) a = f a g a
              instance TopHom.instSupTopHomToTopToLEToPreorderToPartialOrder {α : Type u_1} {β : Type u_2} [inst : Top α] [inst : SemilatticeSup β] [inst : OrderTop β] :
              Sup (TopHom α β)
              Equations
              • TopHom.instSupTopHomToTopToLEToPreorderToPartialOrder = { sup := fun f g => { toFun := f g, map_top' := (_ : ((αβ) Pi.instSupForAll) f g = ) } }
              instance TopHom.instSemilatticeSupTopHomToTopToLEToPreorderToPartialOrder {α : Type u_1} {β : Type u_2} [inst : Top α] [inst : SemilatticeSup β] [inst : OrderTop β] :
              Equations
              • One or more equations did not get rendered due to their size.
              @[simp]
              theorem TopHom.coe_sup {α : Type u_1} {β : Type u_2} [inst : Top α] [inst : SemilatticeSup β] [inst : OrderTop β] (f : TopHom α β) (g : TopHom α β) :
              ↑(f g) = f g
              @[simp]
              theorem TopHom.sup_apply {α : Type u_2} {β : Type u_1} [inst : Top α] [inst : SemilatticeSup β] [inst : OrderTop β] (f : TopHom α β) (g : TopHom α β) (a : α) :
              ↑(f g) a = f a g a
              instance TopHom.instLatticeTopHomToTopToLEToPreorderToPartialOrderToSemilatticeInf {α : Type u_1} {β : Type u_2} [inst : Top α] [inst : Lattice β] [inst : OrderTop β] :
              Lattice (TopHom α β)
              Equations
              • One or more equations did not get rendered due to their size.
              Equations
              • One or more equations did not get rendered due to their size.

              Bot homomorphisms #

              instance BotHom.instBotHomClassBotHom {α : Type u_1} {β : Type u_2} [inst : Bot α] [inst : Bot β] :
              BotHomClass (BotHom α β) α β
              Equations
              theorem BotHom.ext {α : Type u_1} {β : Type u_2} [inst : Bot α] [inst : Bot β] {f : BotHom α β} {g : BotHom α β} (h : ∀ (a : α), f a = g a) :
              f = g
              def BotHom.copy {α : Type u_1} {β : Type u_2} [inst : Bot α] [inst : Bot β] (f : BotHom α β) (f' : αβ) (h : f' = f) :
              BotHom α β

              Copy of a BotHom with a new toFun equal to the old one. Useful to fix definitional equalities.

              Equations
              @[simp]
              theorem BotHom.coe_copy {α : Type u_1} {β : Type u_2} [inst : Bot α] [inst : Bot β] (f : BotHom α β) (f' : αβ) (h : f' = f) :
              ↑(BotHom.copy f f' h) = f'
              theorem BotHom.copy_eq {α : Type u_1} {β : Type u_2} [inst : Bot α] [inst : Bot β] (f : BotHom α β) (f' : αβ) (h : f' = f) :
              BotHom.copy f f' h = f
              instance BotHom.instInhabitedBotHom {α : Type u_1} {β : Type u_2} [inst : Bot α] [inst : Bot β] :
              Equations
              • BotHom.instInhabitedBotHom = { default := { toFun := fun x => , map_bot' := (_ : (fun x => ) = (fun x => ) ) } }
              def BotHom.id (α : Type u_1) [inst : Bot α] :
              BotHom α α

              id as a BotHom.

              Equations
              @[simp]
              theorem BotHom.coe_id (α : Type u_1) [inst : Bot α] :
              ↑(BotHom.id α) = id
              @[simp]
              theorem BotHom.id_apply {α : Type u_1} [inst : Bot α] (a : α) :
              ↑(BotHom.id α) a = a
              def BotHom.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Bot α] [inst : Bot β] [inst : Bot γ] (f : BotHom β γ) (g : BotHom α β) :
              BotHom α γ

              Composition of BotHoms as a BotHom.

              Equations
              @[simp]
              theorem BotHom.coe_comp {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : Bot α] [inst : Bot β] [inst : Bot γ] (f : BotHom β γ) (g : BotHom α β) :
              ↑(BotHom.comp f g) = f g
              @[simp]
              theorem BotHom.comp_apply {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : Bot α] [inst : Bot β] [inst : Bot γ] (f : BotHom β γ) (g : BotHom α β) (a : α) :
              ↑(BotHom.comp f g) a = f (g a)
              @[simp]
              theorem BotHom.comp_assoc {α : Type u_4} {β : Type u_3} {γ : Type u_1} {δ : Type u_2} [inst : Bot α] [inst : Bot β] [inst : Bot γ] [inst : Bot δ] (f : BotHom γ δ) (g : BotHom β γ) (h : BotHom α β) :
              @[simp]
              theorem BotHom.comp_id {α : Type u_1} {β : Type u_2} [inst : Bot α] [inst : Bot β] (f : BotHom α β) :
              @[simp]
              theorem BotHom.id_comp {α : Type u_1} {β : Type u_2} [inst : Bot α] [inst : Bot β] (f : BotHom α β) :
              theorem BotHom.cancel_right {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : Bot α] [inst : Bot β] [inst : Bot γ] {g₁ : BotHom β γ} {g₂ : BotHom β γ} {f : BotHom α β} (hf : Function.Surjective f) :
              BotHom.comp g₁ f = BotHom.comp g₂ f g₁ = g₂
              theorem BotHom.cancel_left {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : Bot α] [inst : Bot β] [inst : Bot γ] {g : BotHom β γ} {f₁ : BotHom α β} {f₂ : BotHom α β} (hg : Function.Injective g) :
              BotHom.comp g f₁ = BotHom.comp g f₂ f₁ = f₂
              instance BotHom.instPreorderBotHom {α : Type u_1} {β : Type u_2} [inst : Bot α] [inst : Preorder β] [inst : Bot β] :
              Equations
              instance BotHom.instPartialOrderBotHom {α : Type u_1} {β : Type u_2} [inst : Bot α] [inst : PartialOrder β] [inst : Bot β] :
              Equations
              instance BotHom.instOrderBotBotHomToBotToLEToLEInstPreorderBotHom {α : Type u_1} {β : Type u_2} [inst : Bot α] [inst : Preorder β] [inst : OrderBot β] :
              Equations
              • BotHom.instOrderBotBotHomToBotToLEToLEInstPreorderBotHom = OrderBot.mk (_ : ∀ (x : BotHom α β), fun i => x i)
              @[simp]
              theorem BotHom.coe_bot {α : Type u_1} {β : Type u_2} [inst : Bot α] [inst : Preorder β] [inst : OrderBot β] :
              =
              @[simp]
              theorem BotHom.bot_apply {α : Type u_2} {β : Type u_1} [inst : Bot α] [inst : Preorder β] [inst : OrderBot β] (a : α) :
              a =
              instance BotHom.instInfBotHomToBotToLEToPreorderToPartialOrder {α : Type u_1} {β : Type u_2} [inst : Bot α] [inst : SemilatticeInf β] [inst : OrderBot β] :
              Inf (BotHom α β)
              Equations
              • BotHom.instInfBotHomToBotToLEToPreorderToPartialOrder = { inf := fun f g => { toFun := f g, map_bot' := (_ : ((αβ) Pi.instInfForAll) f g = ) } }
              instance BotHom.instSemilatticeInfBotHomToBotToLEToPreorderToPartialOrder {α : Type u_1} {β : Type u_2} [inst : Bot α] [inst : SemilatticeInf β] [inst : OrderBot β] :
              Equations
              • One or more equations did not get rendered due to their size.
              @[simp]
              theorem BotHom.coe_inf {α : Type u_1} {β : Type u_2} [inst : Bot α] [inst : SemilatticeInf β] [inst : OrderBot β] (f : BotHom α β) (g : BotHom α β) :
              ↑(f g) = f g
              @[simp]
              theorem BotHom.inf_apply {α : Type u_2} {β : Type u_1} [inst : Bot α] [inst : SemilatticeInf β] [inst : OrderBot β] (f : BotHom α β) (g : BotHom α β) (a : α) :
              ↑(f g) a = f a g a
              instance BotHom.instSupBotHomToBotToLEToPreorderToPartialOrder {α : Type u_1} {β : Type u_2} [inst : Bot α] [inst : SemilatticeSup β] [inst : OrderBot β] :
              Sup (BotHom α β)
              Equations
              • BotHom.instSupBotHomToBotToLEToPreorderToPartialOrder = { sup := fun f g => { toFun := f g, map_bot' := (_ : ((αβ) Pi.instSupForAll) f g = ) } }
              instance BotHom.instSemilatticeSupBotHomToBotToLEToPreorderToPartialOrder {α : Type u_1} {β : Type u_2} [inst : Bot α] [inst : SemilatticeSup β] [inst : OrderBot β] :
              Equations
              • One or more equations did not get rendered due to their size.
              @[simp]
              theorem BotHom.coe_sup {α : Type u_1} {β : Type u_2} [inst : Bot α] [inst : SemilatticeSup β] [inst : OrderBot β] (f : BotHom α β) (g : BotHom α β) :
              ↑(f g) = f g
              @[simp]
              theorem BotHom.sup_apply {α : Type u_2} {β : Type u_1} [inst : Bot α] [inst : SemilatticeSup β] [inst : OrderBot β] (f : BotHom α β) (g : BotHom α β) (a : α) :
              ↑(f g) a = f a g a
              instance BotHom.instLatticeBotHomToBotToLEToPreorderToPartialOrderToSemilatticeInf {α : Type u_1} {β : Type u_2} [inst : Bot α] [inst : Lattice β] [inst : OrderBot β] :
              Lattice (BotHom α β)
              Equations
              • One or more equations did not get rendered due to their size.
              Equations
              • One or more equations did not get rendered due to their size.

              Bounded order homomorphisms #

              def BoundedOrderHom.toTopHom {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : BoundedOrder α] [inst : BoundedOrder β] (f : BoundedOrderHom α β) :
              TopHom α β

              Reinterpret a BoundedOrderHom as a TopHom.

              Equations
              def BoundedOrderHom.toBotHom {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : BoundedOrder α] [inst : BoundedOrder β] (f : BoundedOrderHom α β) :
              BotHom α β

              Reinterpret a BoundedOrderHom as a BotHom.

              Equations
              instance BoundedOrderHom.instBoundedOrderHomClassBoundedOrderHomToLEToLE {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : BoundedOrder α] [inst : BoundedOrder β] :
              Equations
              • One or more equations did not get rendered due to their size.
              theorem BoundedOrderHom.ext {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : BoundedOrder α] [inst : BoundedOrder β] {f : BoundedOrderHom α β} {g : BoundedOrderHom α β} (h : ∀ (a : α), f a = g a) :
              f = g
              def BoundedOrderHom.copy {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : BoundedOrder α] [inst : BoundedOrder β] (f : BoundedOrderHom α β) (f' : αβ) (h : f' = f) :

              Copy of a BoundedOrderHom with a new toFun equal to the old one. Useful to fix definitional equalities.

              Equations
              • One or more equations did not get rendered due to their size.
              @[simp]
              theorem BoundedOrderHom.coe_copy {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : BoundedOrder α] [inst : BoundedOrder β] (f : BoundedOrderHom α β) (f' : αβ) (h : f' = f) :
              ↑(BoundedOrderHom.copy f f' h) = f'
              theorem BoundedOrderHom.copy_eq {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : BoundedOrder α] [inst : BoundedOrder β] (f : BoundedOrderHom α β) (f' : αβ) (h : f' = f) :
              def BoundedOrderHom.id (α : Type u_1) [inst : Preorder α] [inst : BoundedOrder α] :

              id as a BoundedOrderHom.

              Equations
              • One or more equations did not get rendered due to their size.
              @[simp]
              theorem BoundedOrderHom.coe_id (α : Type u_1) [inst : Preorder α] [inst : BoundedOrder α] :
              @[simp]
              theorem BoundedOrderHom.id_apply {α : Type u_1} [inst : Preorder α] [inst : BoundedOrder α] (a : α) :
              ↑(BoundedOrderHom.id α) a = a
              def BoundedOrderHom.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Preorder α] [inst : Preorder β] [inst : Preorder γ] [inst : BoundedOrder α] [inst : BoundedOrder β] [inst : BoundedOrder γ] (f : BoundedOrderHom β γ) (g : BoundedOrderHom α β) :

              Composition of BoundedOrderHoms as a BoundedOrderHom.

              Equations
              • One or more equations did not get rendered due to their size.
              @[simp]
              theorem BoundedOrderHom.coe_comp {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : Preorder γ] [inst : BoundedOrder α] [inst : BoundedOrder β] [inst : BoundedOrder γ] (f : BoundedOrderHom β γ) (g : BoundedOrderHom α β) :
              ↑(BoundedOrderHom.comp f g) = f g
              @[simp]
              theorem BoundedOrderHom.comp_apply {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : Preorder γ] [inst : BoundedOrder α] [inst : BoundedOrder β] [inst : BoundedOrder γ] (f : BoundedOrderHom β γ) (g : BoundedOrderHom α β) (a : α) :
              ↑(BoundedOrderHom.comp f g) a = f (g a)
              @[simp]
              theorem BoundedOrderHom.coe_comp_orderHom {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : Preorder γ] [inst : BoundedOrder α] [inst : BoundedOrder β] [inst : BoundedOrder γ] (f : BoundedOrderHom β γ) (g : BoundedOrderHom α β) :
              @[simp]
              theorem BoundedOrderHom.coe_comp_topHom {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : Preorder γ] [inst : BoundedOrder α] [inst : BoundedOrder β] [inst : BoundedOrder γ] (f : BoundedOrderHom β γ) (g : BoundedOrderHom α β) :
              @[simp]
              theorem BoundedOrderHom.coe_comp_botHom {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : Preorder γ] [inst : BoundedOrder α] [inst : BoundedOrder β] [inst : BoundedOrder γ] (f : BoundedOrderHom β γ) (g : BoundedOrderHom α β) :
              @[simp]
              theorem BoundedOrderHom.comp_assoc {α : Type u_4} {β : Type u_3} {γ : Type u_1} {δ : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : Preorder γ] [inst : Preorder δ] [inst : BoundedOrder α] [inst : BoundedOrder β] [inst : BoundedOrder γ] [inst : BoundedOrder δ] (f : BoundedOrderHom γ δ) (g : BoundedOrderHom β γ) (h : BoundedOrderHom α β) :
              @[simp]
              theorem BoundedOrderHom.comp_id {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : BoundedOrder α] [inst : BoundedOrder β] (f : BoundedOrderHom α β) :
              @[simp]
              theorem BoundedOrderHom.id_comp {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : BoundedOrder α] [inst : BoundedOrder β] (f : BoundedOrderHom α β) :
              theorem BoundedOrderHom.cancel_right {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : Preorder γ] [inst : BoundedOrder α] [inst : BoundedOrder β] [inst : BoundedOrder γ] {g₁ : BoundedOrderHom β γ} {g₂ : BoundedOrderHom β γ} {f : BoundedOrderHom α β} (hf : Function.Surjective f) :
              theorem BoundedOrderHom.cancel_left {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : Preorder γ] [inst : BoundedOrder α] [inst : BoundedOrder β] [inst : BoundedOrder γ] {g : BoundedOrderHom β γ} {f₁ : BoundedOrderHom α β} {f₂ : BoundedOrderHom α β} (hg : Function.Injective g) :

              Dual homs #

              @[simp]
              theorem TopHom.dual_symm_apply_apply {α : Type u_1} {β : Type u_2} [inst : LE α] [inst : OrderTop α] [inst : LE β] [inst : OrderTop β] (f : BotHom αᵒᵈ βᵒᵈ) (a : αᵒᵈ) :
              ↑(↑(Equiv.symm TopHom.dual) f) a = f a
              @[simp]
              theorem TopHom.dual_apply_apply {α : Type u_1} {β : Type u_2} [inst : LE α] [inst : OrderTop α] [inst : LE β] [inst : OrderTop β] (f : TopHom α β) (a : α) :
              ↑(TopHom.dual f) a = f a
              def TopHom.dual {α : Type u_1} {β : Type u_2} [inst : LE α] [inst : OrderTop α] [inst : LE β] [inst : OrderTop β] :

              Reinterpret a top homomorphism as a bot homomorphism between the dual lattices.

              Equations
              • One or more equations did not get rendered due to their size.
              @[simp]
              theorem TopHom.dual_id {α : Type u_1} [inst : LE α] [inst : OrderTop α] :
              TopHom.dual (TopHom.id α) = BotHom.id αᵒᵈ
              @[simp]
              theorem TopHom.dual_comp {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : LE α] [inst : OrderTop α] [inst : LE β] [inst : OrderTop β] [inst : LE γ] [inst : OrderTop γ] (g : TopHom β γ) (f : TopHom α β) :
              TopHom.dual (TopHom.comp g f) = BotHom.comp (TopHom.dual g) (TopHom.dual f)
              @[simp]
              theorem TopHom.symm_dual_id {α : Type u_1} [inst : LE α] [inst : OrderTop α] :
              ↑(Equiv.symm TopHom.dual) (BotHom.id αᵒᵈ) = TopHom.id α
              @[simp]
              theorem TopHom.symm_dual_comp {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : LE α] [inst : OrderTop α] [inst : LE β] [inst : OrderTop β] [inst : LE γ] [inst : OrderTop γ] (g : BotHom βᵒᵈ γᵒᵈ) (f : BotHom αᵒᵈ βᵒᵈ) :
              ↑(Equiv.symm TopHom.dual) (BotHom.comp g f) = TopHom.comp (↑(Equiv.symm TopHom.dual) g) (↑(Equiv.symm TopHom.dual) f)
              @[simp]
              theorem BotHom.dual_apply_apply {α : Type u_1} {β : Type u_2} [inst : LE α] [inst : OrderBot α] [inst : LE β] [inst : OrderBot β] (f : BotHom α β) (a : α) :
              ↑(BotHom.dual f) a = f a
              @[simp]
              theorem BotHom.dual_symm_apply_apply {α : Type u_1} {β : Type u_2} [inst : LE α] [inst : OrderBot α] [inst : LE β] [inst : OrderBot β] (f : TopHom αᵒᵈ βᵒᵈ) (a : αᵒᵈ) :
              ↑(↑(Equiv.symm BotHom.dual) f) a = f a
              def BotHom.dual {α : Type u_1} {β : Type u_2} [inst : LE α] [inst : OrderBot α] [inst : LE β] [inst : OrderBot β] :

              Reinterpret a bot homomorphism as a top homomorphism between the dual lattices.

              Equations
              • One or more equations did not get rendered due to their size.
              @[simp]
              theorem BotHom.dual_id {α : Type u_1} [inst : LE α] [inst : OrderBot α] :
              BotHom.dual (BotHom.id α) = TopHom.id αᵒᵈ
              @[simp]
              theorem BotHom.dual_comp {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : LE α] [inst : OrderBot α] [inst : LE β] [inst : OrderBot β] [inst : LE γ] [inst : OrderBot γ] (g : BotHom β γ) (f : BotHom α β) :
              BotHom.dual (BotHom.comp g f) = TopHom.comp (BotHom.dual g) (BotHom.dual f)
              @[simp]
              theorem BotHom.symm_dual_id {α : Type u_1} [inst : LE α] [inst : OrderBot α] :
              ↑(Equiv.symm BotHom.dual) (TopHom.id αᵒᵈ) = BotHom.id α
              @[simp]
              theorem BotHom.symm_dual_comp {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : LE α] [inst : OrderBot α] [inst : LE β] [inst : OrderBot β] [inst : LE γ] [inst : OrderBot γ] (g : TopHom βᵒᵈ γᵒᵈ) (f : TopHom αᵒᵈ βᵒᵈ) :
              ↑(Equiv.symm BotHom.dual) (TopHom.comp g f) = BotHom.comp (↑(Equiv.symm BotHom.dual) g) (↑(Equiv.symm BotHom.dual) f)
              @[simp]
              theorem BoundedOrderHom.dual_apply_toOrderHom {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : BoundedOrder α] [inst : Preorder β] [inst : BoundedOrder β] (f : BoundedOrderHom α β) :
              (BoundedOrderHom.dual f).toOrderHom = OrderHom.dual f.toOrderHom
              @[simp]
              theorem BoundedOrderHom.dual_symm_apply_toOrderHom {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : BoundedOrder α] [inst : Preorder β] [inst : BoundedOrder β] (f : BoundedOrderHom αᵒᵈ βᵒᵈ) :
              (↑(Equiv.symm BoundedOrderHom.dual) f).toOrderHom = ↑(Equiv.symm OrderHom.dual) f.toOrderHom
              def BoundedOrderHom.dual {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : BoundedOrder α] [inst : Preorder β] [inst : BoundedOrder β] :

              Reinterpret a bounded order homomorphism as a bounded order homomorphism between the dual orders.

              Equations
              • One or more equations did not get rendered due to their size.
              @[simp]
              theorem BoundedOrderHom.dual_id {α : Type u_1} [inst : Preorder α] [inst : BoundedOrder α] :
              BoundedOrderHom.dual (BoundedOrderHom.id α) = BoundedOrderHom.id αᵒᵈ
              @[simp]
              theorem BoundedOrderHom.dual_comp {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : Preorder α] [inst : BoundedOrder α] [inst : Preorder β] [inst : BoundedOrder β] [inst : Preorder γ] [inst : BoundedOrder γ] (g : BoundedOrderHom β γ) (f : BoundedOrderHom α β) :
              BoundedOrderHom.dual (BoundedOrderHom.comp g f) = BoundedOrderHom.comp (BoundedOrderHom.dual g) (BoundedOrderHom.dual f)
              @[simp]
              theorem BoundedOrderHom.symm_dual_id {α : Type u_1} [inst : Preorder α] [inst : BoundedOrder α] :
              ↑(Equiv.symm BoundedOrderHom.dual) (BoundedOrderHom.id αᵒᵈ) = BoundedOrderHom.id α
              @[simp]
              theorem BoundedOrderHom.symm_dual_comp {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : Preorder α] [inst : BoundedOrder α] [inst : Preorder β] [inst : BoundedOrder β] [inst : Preorder γ] [inst : BoundedOrder γ] (g : BoundedOrderHom βᵒᵈ γᵒᵈ) (f : BoundedOrderHom αᵒᵈ βᵒᵈ) :
              ↑(Equiv.symm BoundedOrderHom.dual) (BoundedOrderHom.comp g f) = BoundedOrderHom.comp (↑(Equiv.symm BoundedOrderHom.dual) g) (↑(Equiv.symm BoundedOrderHom.dual) f)