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_6) (β : Type u_7) [Top α] [Top β] :
Type (max u_6 u_7)
  • toFun : αβ

    The underlying function. The preferred spelling is FunLike.coe.

  • map_top' : TopHom.toFun s =

    The function preserves the top element. The preferred spelling is map_top.

The type of -preserving functions from α to β.

Instances For
    structure BotHom (α : Type u_6) (β : Type u_7) [Bot α] [Bot β] :
    Type (max u_6 u_7)
    • toFun : αβ

      The underlying function. The preferred spelling is FunLike.coe.

    • map_bot' : BotHom.toFun s =

      The function preserves the bottom element. The preferred spelling is map_bot.

    The type of -preserving functions from α to β.

    Instances For
      structure BoundedOrderHom (α : Type u_6) (β : Type u_7) [Preorder α] [Preorder β] [BoundedOrder α] [BoundedOrder β] extends OrderHom :
      Type (max u_6 u_7)

      The type of bounded order homomorphisms from α to β.

      Instances For
        class TopHomClass (F : Type u_6) (α : outParam (Type u_7)) (β : outParam (Type u_8)) [Top α] [Top β] extends FunLike :
        Type (max (max u_6 u_7) u_8)

        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_6) (α : outParam (Type u_7)) (β : outParam (Type u_8)) [Bot α] [Bot β] extends FunLike :
          Type (max (max u_6 u_7) u_8)

          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_6) (α : outParam (Type u_7)) (β : outParam (Type u_8)) [LE α] [LE β] [BoundedOrder α] [BoundedOrder β] extends RelHomClass :
            Type (max (max u_6 u_7) u_8)
            • coe : Fαβ
            • coe_injective' : Function.Injective FunLike.coe
            • map_rel : ∀ (f : F) {a b : α}, a bf a f b
            • map_top : ∀ (f : F), f =

              Morphisms preserve the top element. The preferred spelling is _root_.map_top.

            • map_bot : ∀ (f : F), f =

              Morphisms preserve the bottom element. The preferred spelling is _root_.map_bot.

            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} [LE α] [LE β] [BoundedOrder α] [BoundedOrder β] [BoundedOrderHomClass F α β] :
              TopHomClass F α β
              Equations
              instance BoundedOrderHomClass.toBotHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [LE α] [LE β] [BoundedOrder α] [BoundedOrder β] [BoundedOrderHomClass F α β] :
              BotHomClass F α β
              Equations
              instance OrderIsoClass.toTopHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [LE α] [OrderTop α] [PartialOrder β] [OrderTop β] [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} [LE α] [OrderBot α] [PartialOrder β] [OrderBot β] [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} [LE α] [BoundedOrder α] [PartialOrder β] [BoundedOrder β] [OrderIsoClass F α β] :
              Equations
              • One or more equations did not get rendered due to their size.
              @[simp]
              theorem map_eq_top_iff {F : Type u_1} {α : Type u_2} {β : Type u_3} [LE α] [OrderTop α] [PartialOrder β] [OrderTop β] [OrderIsoClass F α β] (f : F) {a : α} :
              f a = a =
              @[simp]
              theorem map_eq_bot_iff {F : Type u_1} {α : Type u_2} {β : Type u_3} [LE α] [OrderBot α] [PartialOrder β] [OrderBot β] [OrderIsoClass F α β] (f : F) {a : α} :
              f a = a =
              def TopHomClass.toTopHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [Top α] [Top β] [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 = ) }
              Instances For
                instance instCoeTCTopHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [Top α] [Top β] [TopHomClass F α β] :
                CoeTC F (TopHom α β)
                Equations
                • instCoeTCTopHom = { coe := TopHomClass.toTopHom }
                def BotHomClass.toBotHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [Bot α] [Bot β] [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 = ) }
                Instances For
                  instance instCoeTCBotHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [Bot α] [Bot β] [BotHomClass F α β] :
                  CoeTC F (BotHom α β)
                  Equations
                  • instCoeTCBotHom = { coe := BotHomClass.toBotHom }
                  def BoundedOrderHomClass.toBoundedOrderHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [BoundedOrder α] [BoundedOrder β] [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.toFun) }, map_top' := (_ : f = ), map_bot' := (_ : f = ) }
                  Instances For
                    instance instCoeTCBoundedOrderHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [BoundedOrder α] [BoundedOrder β] [BoundedOrderHomClass F α β] :
                    Equations
                    • instCoeTCBoundedOrderHom = { coe := BoundedOrderHomClass.toBoundedOrderHom }

                    Top homomorphisms #

                    instance TopHom.instTopHomClassTopHom {α : Type u_2} {β : Type u_3} [Top α] [Top β] :
                    TopHomClass (TopHom α β) α β
                    Equations
                    theorem TopHom.ext {α : Type u_2} {β : Type u_3} [Top α] [Top β] {f : TopHom α β} {g : TopHom α β} (h : ∀ (a : α), f a = g a) :
                    f = g
                    def TopHom.copy {α : Type u_2} {β : Type u_3} [Top α] [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
                    Instances For
                      @[simp]
                      theorem TopHom.coe_copy {α : Type u_2} {β : Type u_3} [Top α] [Top β] (f : TopHom α β) (f' : αβ) (h : f' = f) :
                      ↑(TopHom.copy f f' h) = f'
                      theorem TopHom.copy_eq {α : Type u_2} {β : Type u_3} [Top α] [Top β] (f : TopHom α β) (f' : αβ) (h : f' = f) :
                      TopHom.copy f f' h = f
                      instance TopHom.instInhabitedTopHom {α : Type u_2} {β : Type u_3} [Top α] [Top β] :
                      Equations
                      • TopHom.instInhabitedTopHom = { default := { toFun := fun x => , map_top' := (_ : (fun x => ) = (fun x => ) ) } }
                      def TopHom.id (α : Type u_2) [Top α] :
                      TopHom α α

                      id as a TopHom.

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

                        Composition of TopHoms as a TopHom.

                        Equations
                        Instances For
                          @[simp]
                          theorem TopHom.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Top α] [Top β] [Top γ] (f : TopHom β γ) (g : TopHom α β) :
                          ↑(TopHom.comp f g) = f g
                          @[simp]
                          theorem TopHom.comp_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Top α] [Top β] [Top γ] (f : TopHom β γ) (g : TopHom α β) (a : α) :
                          ↑(TopHom.comp f g) a = f (g a)
                          @[simp]
                          theorem TopHom.comp_assoc {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [Top α] [Top β] [Top γ] [Top δ] (f : TopHom γ δ) (g : TopHom β γ) (h : TopHom α β) :
                          @[simp]
                          theorem TopHom.comp_id {α : Type u_2} {β : Type u_3} [Top α] [Top β] (f : TopHom α β) :
                          @[simp]
                          theorem TopHom.id_comp {α : Type u_2} {β : Type u_3} [Top α] [Top β] (f : TopHom α β) :
                          @[simp]
                          theorem TopHom.cancel_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Top α] [Top β] [Top γ] {g₁ : TopHom β γ} {g₂ : TopHom β γ} {f : TopHom α β} (hf : Function.Surjective f) :
                          TopHom.comp g₁ f = TopHom.comp g₂ f g₁ = g₂
                          @[simp]
                          theorem TopHom.cancel_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Top α] [Top β] [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_2} {β : Type u_3} [Top α] [Preorder β] [Top β] :
                          Equations
                          instance TopHom.instPartialOrderTopHom {α : Type u_2} {β : Type u_3} [Top α] [PartialOrder β] [Top β] :
                          Equations
                          Equations
                          • TopHom.instOrderTopTopHomToTopToLEToLEInstPreorderTopHom = OrderTop.mk (_ : ∀ (x : TopHom α β), (fun i => x i) )
                          @[simp]
                          theorem TopHom.coe_top {α : Type u_2} {β : Type u_3} [Top α] [Preorder β] [OrderTop β] :
                          =
                          @[simp]
                          theorem TopHom.top_apply {α : Type u_2} {β : Type u_3} [Top α] [Preorder β] [OrderTop β] (a : α) :
                          a =
                          Equations
                          • TopHom.instInfTopHomToTopToLEToPreorderToPartialOrder = { inf := fun f g => { toFun := f g, map_top' := (_ : ((αβ) Pi.instInfForAll) f g = ) } }
                          Equations
                          • One or more equations did not get rendered due to their size.
                          @[simp]
                          theorem TopHom.coe_inf {α : Type u_2} {β : Type u_3} [Top α] [SemilatticeInf β] [OrderTop β] (f : TopHom α β) (g : TopHom α β) :
                          ↑(f g) = f g
                          @[simp]
                          theorem TopHom.inf_apply {α : Type u_2} {β : Type u_3} [Top α] [SemilatticeInf β] [OrderTop β] (f : TopHom α β) (g : TopHom α β) (a : α) :
                          ↑(f g) a = f a g a
                          Equations
                          • TopHom.instSupTopHomToTopToLEToPreorderToPartialOrder = { sup := fun f g => { toFun := f g, map_top' := (_ : ((αβ) Pi.instSupForAll) f g = ) } }
                          Equations
                          • One or more equations did not get rendered due to their size.
                          @[simp]
                          theorem TopHom.coe_sup {α : Type u_2} {β : Type u_3} [Top α] [SemilatticeSup β] [OrderTop β] (f : TopHom α β) (g : TopHom α β) :
                          ↑(f g) = f g
                          @[simp]
                          theorem TopHom.sup_apply {α : Type u_2} {β : Type u_3} [Top α] [SemilatticeSup β] [OrderTop β] (f : TopHom α β) (g : TopHom α β) (a : α) :
                          ↑(f g) a = f a g a
                          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_2} {β : Type u_3} [Bot α] [Bot β] :
                          BotHomClass (BotHom α β) α β
                          Equations
                          theorem BotHom.ext {α : Type u_2} {β : Type u_3} [Bot α] [Bot β] {f : BotHom α β} {g : BotHom α β} (h : ∀ (a : α), f a = g a) :
                          f = g
                          def BotHom.copy {α : Type u_2} {β : Type u_3} [Bot α] [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
                          Instances For
                            @[simp]
                            theorem BotHom.coe_copy {α : Type u_2} {β : Type u_3} [Bot α] [Bot β] (f : BotHom α β) (f' : αβ) (h : f' = f) :
                            ↑(BotHom.copy f f' h) = f'
                            theorem BotHom.copy_eq {α : Type u_2} {β : Type u_3} [Bot α] [Bot β] (f : BotHom α β) (f' : αβ) (h : f' = f) :
                            BotHom.copy f f' h = f
                            instance BotHom.instInhabitedBotHom {α : Type u_2} {β : Type u_3} [Bot α] [Bot β] :
                            Equations
                            • BotHom.instInhabitedBotHom = { default := { toFun := fun x => , map_bot' := (_ : (fun x => ) = (fun x => ) ) } }
                            def BotHom.id (α : Type u_2) [Bot α] :
                            BotHom α α

                            id as a BotHom.

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

                              Composition of BotHoms as a BotHom.

                              Equations
                              Instances For
                                @[simp]
                                theorem BotHom.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Bot α] [Bot β] [Bot γ] (f : BotHom β γ) (g : BotHom α β) :
                                ↑(BotHom.comp f g) = f g
                                @[simp]
                                theorem BotHom.comp_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Bot α] [Bot β] [Bot γ] (f : BotHom β γ) (g : BotHom α β) (a : α) :
                                ↑(BotHom.comp f g) a = f (g a)
                                @[simp]
                                theorem BotHom.comp_assoc {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [Bot α] [Bot β] [Bot γ] [Bot δ] (f : BotHom γ δ) (g : BotHom β γ) (h : BotHom α β) :
                                @[simp]
                                theorem BotHom.comp_id {α : Type u_2} {β : Type u_3} [Bot α] [Bot β] (f : BotHom α β) :
                                @[simp]
                                theorem BotHom.id_comp {α : Type u_2} {β : Type u_3} [Bot α] [Bot β] (f : BotHom α β) :
                                @[simp]
                                theorem BotHom.cancel_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Bot α] [Bot β] [Bot γ] {g₁ : BotHom β γ} {g₂ : BotHom β γ} {f : BotHom α β} (hf : Function.Surjective f) :
                                BotHom.comp g₁ f = BotHom.comp g₂ f g₁ = g₂
                                @[simp]
                                theorem BotHom.cancel_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Bot α] [Bot β] [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_2} {β : Type u_3} [Bot α] [Preorder β] [Bot β] :
                                Equations
                                instance BotHom.instPartialOrderBotHom {α : Type u_2} {β : Type u_3} [Bot α] [PartialOrder β] [Bot β] :
                                Equations
                                Equations
                                • BotHom.instOrderBotBotHomToBotToLEToLEInstPreorderBotHom = OrderBot.mk (_ : ∀ (x : BotHom α β), fun i => x i)
                                @[simp]
                                theorem BotHom.coe_bot {α : Type u_2} {β : Type u_3} [Bot α] [Preorder β] [OrderBot β] :
                                =
                                @[simp]
                                theorem BotHom.bot_apply {α : Type u_2} {β : Type u_3} [Bot α] [Preorder β] [OrderBot β] (a : α) :
                                a =
                                Equations
                                • BotHom.instInfBotHomToBotToLEToPreorderToPartialOrder = { inf := fun f g => { toFun := f g, map_bot' := (_ : ((αβ) Pi.instInfForAll) f g = ) } }
                                Equations
                                • One or more equations did not get rendered due to their size.
                                @[simp]
                                theorem BotHom.coe_inf {α : Type u_2} {β : Type u_3} [Bot α] [SemilatticeInf β] [OrderBot β] (f : BotHom α β) (g : BotHom α β) :
                                ↑(f g) = f g
                                @[simp]
                                theorem BotHom.inf_apply {α : Type u_2} {β : Type u_3} [Bot α] [SemilatticeInf β] [OrderBot β] (f : BotHom α β) (g : BotHom α β) (a : α) :
                                ↑(f g) a = f a g a
                                Equations
                                • BotHom.instSupBotHomToBotToLEToPreorderToPartialOrder = { sup := fun f g => { toFun := f g, map_bot' := (_ : ((αβ) Pi.instSupForAll) f g = ) } }
                                Equations
                                • One or more equations did not get rendered due to their size.
                                @[simp]
                                theorem BotHom.coe_sup {α : Type u_2} {β : Type u_3} [Bot α] [SemilatticeSup β] [OrderBot β] (f : BotHom α β) (g : BotHom α β) :
                                ↑(f g) = f g
                                @[simp]
                                theorem BotHom.sup_apply {α : Type u_2} {β : Type u_3} [Bot α] [SemilatticeSup β] [OrderBot β] (f : BotHom α β) (g : BotHom α β) (a : α) :
                                ↑(f g) a = f a g a
                                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_2} {β : Type u_3} [Preorder α] [Preorder β] [BoundedOrder α] [BoundedOrder β] (f : BoundedOrderHom α β) :
                                TopHom α β

                                Reinterpret a BoundedOrderHom as a TopHom.

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

                                  Reinterpret a BoundedOrderHom as a BotHom.

                                  Equations
                                  Instances For
                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    theorem BoundedOrderHom.ext {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [BoundedOrder α] [BoundedOrder β] {f : BoundedOrderHom α β} {g : BoundedOrderHom α β} (h : ∀ (a : α), f a = g a) :
                                    f = g
                                    def BoundedOrderHom.copy {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [BoundedOrder α] [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.
                                    Instances For
                                      @[simp]
                                      theorem BoundedOrderHom.coe_copy {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [BoundedOrder α] [BoundedOrder β] (f : BoundedOrderHom α β) (f' : αβ) (h : f' = f) :
                                      ↑(BoundedOrderHom.copy f f' h) = f'
                                      theorem BoundedOrderHom.copy_eq {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [BoundedOrder α] [BoundedOrder β] (f : BoundedOrderHom α β) (f' : αβ) (h : f' = f) :

                                      id as a BoundedOrderHom.

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

                                        Composition of BoundedOrderHoms as a BoundedOrderHom.

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

                                          Dual homs #

                                          @[simp]
                                          theorem TopHom.dual_symm_apply_apply {α : Type u_2} {β : Type u_3} [LE α] [OrderTop α] [LE β] [OrderTop β] (f : BotHom αᵒᵈ βᵒᵈ) (a : αᵒᵈ) :
                                          ↑(TopHom.dual.symm f) a = f a
                                          @[simp]
                                          theorem TopHom.dual_apply_apply {α : Type u_2} {β : Type u_3} [LE α] [OrderTop α] [LE β] [OrderTop β] (f : TopHom α β) (a : α) :
                                          ↑(TopHom.dual f) a = f a
                                          def TopHom.dual {α : Type u_2} {β : Type u_3} [LE α] [OrderTop α] [LE β] [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.
                                          Instances For
                                            @[simp]
                                            theorem TopHom.dual_id {α : Type u_2} [LE α] [OrderTop α] :
                                            TopHom.dual (TopHom.id α) = BotHom.id αᵒᵈ
                                            @[simp]
                                            theorem TopHom.dual_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [LE α] [OrderTop α] [LE β] [OrderTop β] [LE γ] [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_2} [LE α] [OrderTop α] :
                                            TopHom.dual.symm (BotHom.id αᵒᵈ) = TopHom.id α
                                            @[simp]
                                            theorem TopHom.symm_dual_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [LE α] [OrderTop α] [LE β] [OrderTop β] [LE γ] [OrderTop γ] (g : BotHom βᵒᵈ γᵒᵈ) (f : BotHom αᵒᵈ βᵒᵈ) :
                                            TopHom.dual.symm (BotHom.comp g f) = TopHom.comp (TopHom.dual.symm g) (TopHom.dual.symm f)
                                            @[simp]
                                            theorem BotHom.dual_apply_apply {α : Type u_2} {β : Type u_3} [LE α] [OrderBot α] [LE β] [OrderBot β] (f : BotHom α β) (a : α) :
                                            ↑(BotHom.dual f) a = f a
                                            @[simp]
                                            theorem BotHom.dual_symm_apply_apply {α : Type u_2} {β : Type u_3} [LE α] [OrderBot α] [LE β] [OrderBot β] (f : TopHom αᵒᵈ βᵒᵈ) (a : αᵒᵈ) :
                                            ↑(BotHom.dual.symm f) a = f a
                                            def BotHom.dual {α : Type u_2} {β : Type u_3} [LE α] [OrderBot α] [LE β] [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.
                                            Instances For
                                              @[simp]
                                              theorem BotHom.dual_id {α : Type u_2} [LE α] [OrderBot α] :
                                              BotHom.dual (BotHom.id α) = TopHom.id αᵒᵈ
                                              @[simp]
                                              theorem BotHom.dual_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [LE α] [OrderBot α] [LE β] [OrderBot β] [LE γ] [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_2} [LE α] [OrderBot α] :
                                              BotHom.dual.symm (TopHom.id αᵒᵈ) = BotHom.id α
                                              @[simp]
                                              theorem BotHom.symm_dual_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [LE α] [OrderBot α] [LE β] [OrderBot β] [LE γ] [OrderBot γ] (g : TopHom βᵒᵈ γᵒᵈ) (f : TopHom αᵒᵈ βᵒᵈ) :
                                              BotHom.dual.symm (TopHom.comp g f) = BotHom.comp (BotHom.dual.symm g) (BotHom.dual.symm f)
                                              @[simp]
                                              theorem BoundedOrderHom.dual_apply_toOrderHom {α : Type u_2} {β : Type u_3} [Preorder α] [BoundedOrder α] [Preorder β] [BoundedOrder β] (f : BoundedOrderHom α β) :
                                              (BoundedOrderHom.dual f).toOrderHom = OrderHom.dual f.toOrderHom
                                              @[simp]
                                              theorem BoundedOrderHom.dual_symm_apply_toOrderHom {α : Type u_2} {β : Type u_3} [Preorder α] [BoundedOrder α] [Preorder β] [BoundedOrder β] (f : BoundedOrderHom αᵒᵈ βᵒᵈ) :
                                              (BoundedOrderHom.dual.symm f).toOrderHom = OrderHom.dual.symm f.toOrderHom

                                              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.
                                              Instances For
                                                @[simp]
                                                theorem BoundedOrderHom.dual_id {α : Type u_2} [Preorder α] [BoundedOrder α] :
                                                BoundedOrderHom.dual (BoundedOrderHom.id α) = BoundedOrderHom.id αᵒᵈ
                                                @[simp]
                                                theorem BoundedOrderHom.dual_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [BoundedOrder α] [Preorder β] [BoundedOrder β] [Preorder γ] [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_2} [Preorder α] [BoundedOrder α] :
                                                BoundedOrderHom.dual.symm (BoundedOrderHom.id αᵒᵈ) = BoundedOrderHom.id α
                                                @[simp]
                                                theorem BoundedOrderHom.symm_dual_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [BoundedOrder α] [Preorder β] [BoundedOrder β] [Preorder γ] [BoundedOrder γ] (g : BoundedOrderHom βᵒᵈ γᵒᵈ) (f : BoundedOrderHom αᵒᵈ βᵒᵈ) :
                                                BoundedOrderHom.dual.symm (BoundedOrderHom.comp g f) = BoundedOrderHom.comp (BoundedOrderHom.dual.symm g) (BoundedOrderHom.dual.symm f)