Documentation

Mathlib.Order.Hom.Bounded

Bounded order homomorphisms #

This file defines (bounded) order homomorphisms.

We use the DFunLike 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)

The type of -preserving functions from α to β.

  • toFun : αβ

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

  • map_top' : self.toFun =

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

Instances For
    theorem TopHom.map_top' {α : Type u_6} {β : Type u_7} [Top α] [Top β] (self : TopHom α β) :
    self.toFun =

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

    structure BotHom (α : Type u_6) (β : Type u_7) [Bot α] [Bot β] :
    Type (max u_6 u_7)

    The type of -preserving functions from α to β.

    • toFun : αβ

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

    • map_bot' : self.toFun =

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

    Instances For
      theorem BotHom.map_bot' {α : Type u_6} {β : Type u_7} [Bot α] [Bot β] (self : BotHom α β) :
      self.toFun =

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

      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 β.

      • toFun : αβ
      • monotone' : Monotone self.toFun
      • map_top' : self.toFun =

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

      • map_bot' : self.toFun =

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

      Instances For
        theorem BoundedOrderHom.map_top' {α : Type u_6} {β : Type u_7} [Preorder α] [Preorder β] [BoundedOrder α] [BoundedOrder β] (self : BoundedOrderHom α β) :
        self.toFun =

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

        theorem BoundedOrderHom.map_bot' {α : Type u_6} {β : Type u_7} [Preorder α] [Preorder β] [BoundedOrder α] [BoundedOrder β] (self : BoundedOrderHom α β) :
        self.toFun =

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

        class TopHomClass (F : Type u_6) (α : Type u_7) (β : Type u_8) [Top α] [Top β] [FunLike F α β] :

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

        You should extend this class when you extend TopHom.

        Instances
          @[simp]
          theorem TopHomClass.map_top {F : Type u_6} {α : Type u_7} {β : Type u_8} [Top α] [Top β] [FunLike F α β] [self : TopHomClass F α β] (f : F) :

          A TopHomClass morphism preserves the top element.

          class BotHomClass (F : Type u_6) (α : Type u_7) (β : Type u_8) [Bot α] [Bot β] [FunLike F α β] :

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

          You should extend this class when you extend BotHom.

          Instances
            @[simp]
            theorem BotHomClass.map_bot {F : Type u_6} {α : Type u_7} {β : Type u_8} [Bot α] [Bot β] [FunLike F α β] [self : BotHomClass F α β] (f : F) :

            A BotHomClass morphism preserves the bottom element.

            class BoundedOrderHomClass (F : Type u_6) (α : Type u_7) (β : Type u_8) [LE α] [LE β] [BoundedOrder α] [BoundedOrder β] [FunLike F α β] extends RelHomClass :

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

            You should extend this class when you extend BoundedOrderHom.

            • 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.

            Instances
              theorem BoundedOrderHomClass.map_top {F : Type u_6} {α : Type u_7} {β : Type u_8} [LE α] [LE β] [BoundedOrder α] [BoundedOrder β] [FunLike F α β] [self : BoundedOrderHomClass F α β] (f : F) :

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

              theorem BoundedOrderHomClass.map_bot {F : Type u_6} {α : Type u_7} {β : Type u_8} [LE α] [LE β] [BoundedOrder α] [BoundedOrder β] [FunLike F α β] [self : BoundedOrderHomClass F α β] (f : F) :

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

              @[instance 100]
              instance BoundedOrderHomClass.toTopHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [LE α] [LE β] [BoundedOrder α] [BoundedOrder β] [BoundedOrderHomClass F α β] :
              TopHomClass F α β
              Equations
              • =
              @[instance 100]
              instance BoundedOrderHomClass.toBotHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [LE α] [LE β] [BoundedOrder α] [BoundedOrder β] [BoundedOrderHomClass F α β] :
              BotHomClass F α β
              Equations
              • =
              @[instance 100]
              instance OrderIsoClass.toTopHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [EquivLike F α β] [LE α] [OrderTop α] [PartialOrder β] [OrderTop β] [OrderIsoClass F α β] :
              TopHomClass F α β
              Equations
              • =
              @[instance 100]
              instance OrderIsoClass.toBotHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [EquivLike F α β] [LE α] [OrderBot α] [PartialOrder β] [OrderBot β] [OrderIsoClass F α β] :
              BotHomClass F α β
              Equations
              • =
              @[instance 100]
              instance OrderIsoClass.toBoundedOrderHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [EquivLike F α β] [LE α] [BoundedOrder α] [PartialOrder β] [BoundedOrder β] [OrderIsoClass F α β] :
              Equations
              • =
              @[simp]
              theorem map_eq_top_iff {F : Type u_1} {α : Type u_2} {β : Type u_3} [EquivLike F α β] [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} [EquivLike F α β] [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} [FunLike F α β] [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' := }
              Instances For
                instance instCoeTCTopHomOfTopHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Top α] [Top β] [TopHomClass F α β] :
                CoeTC F (TopHom α β)
                Equations
                • instCoeTCTopHomOfTopHomClass = { coe := TopHomClass.toTopHom }
                def BotHomClass.toBotHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [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' := }
                Instances For
                  instance instCoeTCBotHomOfBotHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Bot α] [Bot β] [BotHomClass F α β] :
                  CoeTC F (BotHom α β)
                  Equations
                  • instCoeTCBotHomOfBotHomClass = { coe := BotHomClass.toBotHom }
                  def BoundedOrderHomClass.toBoundedOrderHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [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 = { toFun := f, monotone' := , map_top' := , map_bot' := }
                  Instances For
                    instance instCoeTCBoundedOrderHomOfBoundedOrderHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Preorder α] [Preorder β] [BoundedOrder α] [BoundedOrder β] [BoundedOrderHomClass F α β] :
                    Equations
                    • instCoeTCBoundedOrderHomOfBoundedOrderHomClass = { coe := BoundedOrderHomClass.toBoundedOrderHom }

                    Top homomorphisms #

                    instance TopHom.instFunLike {α : Type u_2} {β : Type u_3} [Top α] [Top β] :
                    FunLike (TopHom α β) α β
                    Equations
                    • TopHom.instFunLike = { coe := TopHom.toFun, coe_injective' := }
                    instance TopHom.instTopHomClass {α : Type u_2} {β : Type u_3} [Top α] [Top β] :
                    TopHomClass (TopHom α β) α β
                    Equations
                    • =
                    theorem TopHom.ext_iff {α : Type u_2} {β : Type u_3} [Top α] [Top β] {f : TopHom α β} {g : TopHom α β} :
                    f = g ∀ (a : α), f a = g a
                    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
                    • f.copy f' h = { toFun := f', map_top' := }
                    Instances For
                      @[simp]
                      theorem TopHom.coe_copy {α : Type u_2} {β : Type u_3} [Top α] [Top β] (f : TopHom α β) (f' : αβ) (h : f' = f) :
                      (f.copy f' h) = f'
                      theorem TopHom.copy_eq {α : Type u_2} {β : Type u_3} [Top α] [Top β] (f : TopHom α β) (f' : αβ) (h : f' = f) :
                      f.copy f' h = f
                      instance TopHom.instInhabited {α : Type u_2} {β : Type u_3} [Top α] [Top β] :
                      Equations
                      • TopHom.instInhabited = { default := { toFun := fun (x : α) => , map_top' := } }
                      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
                        • f.comp g = { toFun := f g, map_top' := }
                        Instances For
                          @[simp]
                          theorem TopHom.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Top α] [Top β] [Top γ] (f : TopHom β γ) (g : TopHom α β) :
                          (f.comp 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 : α) :
                          (f.comp 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 α β) :
                          (f.comp g).comp h = f.comp (g.comp h)
                          @[simp]
                          theorem TopHom.comp_id {α : Type u_2} {β : Type u_3} [Top α] [Top β] (f : TopHom α β) :
                          f.comp (TopHom.id α) = f
                          @[simp]
                          theorem TopHom.id_comp {α : Type u_2} {β : Type u_3} [Top α] [Top β] (f : TopHom α β) :
                          (TopHom.id β).comp f = f
                          @[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) :
                          g₁.comp f = g₂.comp 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) :
                          g.comp f₁ = g.comp f₂ f₁ = f₂
                          instance TopHom.instLE {α : Type u_2} {β : Type u_3} [Top α] [LE β] [Top β] :
                          LE (TopHom α β)
                          Equations
                          • TopHom.instLE = { le := fun (f g : TopHom α β) => f g }
                          instance TopHom.instPreorder {α : Type u_2} {β : Type u_3} [Top α] [Preorder β] [Top β] :
                          Equations
                          instance TopHom.instPartialOrder {α : Type u_2} {β : Type u_3} [Top α] [PartialOrder β] [Top β] :
                          Equations
                          instance TopHom.instOrderTop {α : Type u_2} {β : Type u_3} [Top α] [LE β] [OrderTop β] :
                          Equations
                          @[simp]
                          theorem TopHom.coe_top {α : Type u_2} {β : Type u_3} [Top α] [LE β] [OrderTop β] :
                          =
                          @[simp]
                          theorem TopHom.top_apply {α : Type u_2} {β : Type u_3} [Top α] [LE β] [OrderTop β] (a : α) :
                          instance TopHom.instInf {α : Type u_2} {β : Type u_3} [Top α] [SemilatticeInf β] [OrderTop β] :
                          Inf (TopHom α β)
                          Equations
                          • TopHom.instInf = { inf := fun (f g : TopHom α β) => { toFun := f g, map_top' := } }
                          instance TopHom.instSemilatticeInf {α : Type u_2} {β : Type u_3} [Top α] [SemilatticeInf β] [OrderTop β] :
                          Equations
                          @[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
                          instance TopHom.instSup {α : Type u_2} {β : Type u_3} [Top α] [SemilatticeSup β] [OrderTop β] :
                          Sup (TopHom α β)
                          Equations
                          • TopHom.instSup = { sup := fun (f g : TopHom α β) => { toFun := f g, map_top' := } }
                          instance TopHom.instSemilatticeSup {α : Type u_2} {β : Type u_3} [Top α] [SemilatticeSup β] [OrderTop β] :
                          Equations
                          @[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
                          instance TopHom.instLattice {α : Type u_2} {β : Type u_3} [Top α] [Lattice β] [OrderTop β] :
                          Lattice (TopHom α β)
                          Equations
                          instance TopHom.instDistribLattice {α : Type u_2} {β : Type u_3} [Top α] [DistribLattice β] [OrderTop β] :
                          Equations

                          Bot homomorphisms #

                          instance BotHom.instFunLike {α : Type u_2} {β : Type u_3} [Bot α] [Bot β] :
                          FunLike (BotHom α β) α β
                          Equations
                          • BotHom.instFunLike = { coe := BotHom.toFun, coe_injective' := }
                          instance BotHom.instBotHomClass {α : Type u_2} {β : Type u_3} [Bot α] [Bot β] :
                          BotHomClass (BotHom α β) α β
                          Equations
                          • =
                          theorem BotHom.ext_iff {α : Type u_2} {β : Type u_3} [Bot α] [Bot β] {f : BotHom α β} {g : BotHom α β} :
                          f = g ∀ (a : α), f a = g a
                          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
                          • f.copy f' h = { toFun := f', map_bot' := }
                          Instances For
                            @[simp]
                            theorem BotHom.coe_copy {α : Type u_2} {β : Type u_3} [Bot α] [Bot β] (f : BotHom α β) (f' : αβ) (h : f' = f) :
                            (f.copy f' h) = f'
                            theorem BotHom.copy_eq {α : Type u_2} {β : Type u_3} [Bot α] [Bot β] (f : BotHom α β) (f' : αβ) (h : f' = f) :
                            f.copy f' h = f
                            instance BotHom.instInhabited {α : Type u_2} {β : Type u_3} [Bot α] [Bot β] :
                            Equations
                            • BotHom.instInhabited = { default := { toFun := fun (x : α) => , map_bot' := } }
                            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
                              • f.comp g = { toFun := f g, map_bot' := }
                              Instances For
                                @[simp]
                                theorem BotHom.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Bot α] [Bot β] [Bot γ] (f : BotHom β γ) (g : BotHom α β) :
                                (f.comp 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 : α) :
                                (f.comp 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 α β) :
                                (f.comp g).comp h = f.comp (g.comp h)
                                @[simp]
                                theorem BotHom.comp_id {α : Type u_2} {β : Type u_3} [Bot α] [Bot β] (f : BotHom α β) :
                                f.comp (BotHom.id α) = f
                                @[simp]
                                theorem BotHom.id_comp {α : Type u_2} {β : Type u_3} [Bot α] [Bot β] (f : BotHom α β) :
                                (BotHom.id β).comp f = f
                                @[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) :
                                g₁.comp f = g₂.comp 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) :
                                g.comp f₁ = g.comp f₂ f₁ = f₂
                                instance BotHom.instLE {α : Type u_2} {β : Type u_3} [Bot α] [LE β] [Bot β] :
                                LE (BotHom α β)
                                Equations
                                • BotHom.instLE = { le := fun (f g : BotHom α β) => f g }
                                instance BotHom.instPreorder {α : Type u_2} {β : Type u_3} [Bot α] [Preorder β] [Bot β] :
                                Equations
                                instance BotHom.instPartialOrder {α : Type u_2} {β : Type u_3} [Bot α] [PartialOrder β] [Bot β] :
                                Equations
                                instance BotHom.instOrderBot {α : Type u_2} {β : Type u_3} [Bot α] [LE β] [OrderBot β] :
                                Equations
                                @[simp]
                                theorem BotHom.coe_bot {α : Type u_2} {β : Type u_3} [Bot α] [LE β] [OrderBot β] :
                                =
                                @[simp]
                                theorem BotHom.bot_apply {α : Type u_2} {β : Type u_3} [Bot α] [LE β] [OrderBot β] (a : α) :
                                instance BotHom.instInf {α : Type u_2} {β : Type u_3} [Bot α] [SemilatticeInf β] [OrderBot β] :
                                Inf (BotHom α β)
                                Equations
                                • BotHom.instInf = { inf := fun (f g : BotHom α β) => { toFun := f g, map_bot' := } }
                                instance BotHom.instSemilatticeInf {α : Type u_2} {β : Type u_3} [Bot α] [SemilatticeInf β] [OrderBot β] :
                                Equations
                                @[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
                                instance BotHom.instSup {α : Type u_2} {β : Type u_3} [Bot α] [SemilatticeSup β] [OrderBot β] :
                                Sup (BotHom α β)
                                Equations
                                • BotHom.instSup = { sup := fun (f g : BotHom α β) => { toFun := f g, map_bot' := } }
                                instance BotHom.instSemilatticeSup {α : Type u_2} {β : Type u_3} [Bot α] [SemilatticeSup β] [OrderBot β] :
                                Equations
                                @[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
                                instance BotHom.instLattice {α : Type u_2} {β : Type u_3} [Bot α] [Lattice β] [OrderBot β] :
                                Lattice (BotHom α β)
                                Equations
                                instance BotHom.instDistribLattice {α : Type u_2} {β : Type u_3} [Bot α] [DistribLattice β] [OrderBot β] :
                                Equations

                                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
                                • f.toTopHom = { toFun := f.toFun, map_top' := }
                                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
                                  • f.toBotHom = { toFun := f.toFun, map_bot' := }
                                  Instances For
                                    instance BoundedOrderHom.instFunLike {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [BoundedOrder α] [BoundedOrder β] :
                                    FunLike (BoundedOrderHom α β) α β
                                    Equations
                                    • BoundedOrderHom.instFunLike = { coe := fun (f : BoundedOrderHom α β) => f.toFun, coe_injective' := }
                                    Equations
                                    • =
                                    theorem BoundedOrderHom.ext_iff {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [BoundedOrder α] [BoundedOrder β] {f : BoundedOrderHom α β} {g : BoundedOrderHom α β} :
                                    f = g ∀ (a : α), f a = g a
                                    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
                                    • f.copy f' h = { toOrderHom := f.copy f' h, map_top' := , map_bot' := }
                                    Instances For
                                      @[simp]
                                      theorem BoundedOrderHom.coe_copy {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [BoundedOrder α] [BoundedOrder β] (f : BoundedOrderHom α β) (f' : αβ) (h : f' = f) :
                                      (f.copy f' h) = f'
                                      theorem BoundedOrderHom.copy_eq {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [BoundedOrder α] [BoundedOrder β] (f : BoundedOrderHom α β) (f' : αβ) (h : f' = f) :
                                      f.copy f' h = f

                                      id as a BoundedOrderHom.

                                      Equations
                                      Instances For
                                        @[simp]
                                        theorem BoundedOrderHom.coe_id (α : Type u_2) [Preorder α] [BoundedOrder α] :
                                        @[simp]
                                        theorem BoundedOrderHom.id_apply {α : Type u_2} [Preorder α] [BoundedOrder α] (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
                                        • f.comp g = { toOrderHom := f.comp g.toOrderHom, map_top' := , map_bot' := }
                                        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 α β) :
                                          (f.comp 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 : α) :
                                          (f.comp 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 α β) :
                                          (f.comp g) = (↑f).comp g
                                          @[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 α β) :
                                          (f.comp g) = (↑f).comp g
                                          @[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 α β) :
                                          (f.comp g) = (↑f).comp g
                                          @[simp]
                                          theorem BoundedOrderHom.comp_assoc {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [Preorder α] [Preorder β] [Preorder γ] [Preorder δ] [BoundedOrder α] [BoundedOrder β] [BoundedOrder γ] [BoundedOrder δ] (f : BoundedOrderHom γ δ) (g : BoundedOrderHom β γ) (h : BoundedOrderHom α β) :
                                          (f.comp g).comp h = f.comp (g.comp h)
                                          @[simp]
                                          theorem BoundedOrderHom.comp_id {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [BoundedOrder α] [BoundedOrder β] (f : BoundedOrderHom α β) :
                                          f.comp (BoundedOrderHom.id α) = f
                                          @[simp]
                                          theorem BoundedOrderHom.id_comp {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [BoundedOrder α] [BoundedOrder β] (f : BoundedOrderHom α β) :
                                          (BoundedOrderHom.id β).comp f = f
                                          @[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) :
                                          g₁.comp f = g₂.comp f g₁ = g₂
                                          @[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) :
                                          g.comp f₁ = g.comp f₂ f₁ = f₂

                                          Dual homs #

                                          @[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
                                          @[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
                                          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
                                          • TopHom.dual = { toFun := fun (f : TopHom α β) => { toFun := f, map_bot' := }, invFun := fun (f : BotHom αᵒᵈ βᵒᵈ) => { toFun := f, map_top' := }, left_inv := , right_inv := }
                                          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 (g.comp f) = (TopHom.dual g).comp (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 (g.comp f) = (TopHom.dual.symm g).comp (TopHom.dual.symm f)
                                            @[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
                                            @[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
                                            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
                                            • BotHom.dual = { toFun := fun (f : BotHom α β) => { toFun := f, map_top' := }, invFun := fun (f : TopHom αᵒᵈ βᵒᵈ) => { toFun := f, map_bot' := }, left_inv := , right_inv := }
                                            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 (g.comp f) = (BotHom.dual g).comp (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 (g.comp f) = (BotHom.dual.symm g).comp (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 (g.comp f) = (BoundedOrderHom.dual g).comp (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 (g.comp f) = (BoundedOrderHom.dual.symm g).comp (BoundedOrderHom.dual.symm f)