Documentation

Mathlib.Order.Hom.Lattice

Lattice homomorphisms #

This file defines (bounded) lattice 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 #

TODO #

Do we need more intersections between BotHom, TopHom and lattice homomorphisms?

structure SupHom (α : Type u_7) (β : Type u_8) [Max α] [Max β] :
Type (max u_7 u_8)

The type of -preserving functions from α to β.

  • toFun : αβ

    The underlying function of a SupHom

  • map_sup' : ∀ (a b : α), self.toFun (a b) = self.toFun a self.toFun b

    A SupHom preserves suprema.

Instances For
    theorem SupHom.map_sup' {α : Type u_7} {β : Type u_8} [Max α] [Max β] (self : SupHom α β) (a : α) (b : α) :
    self.toFun (a b) = self.toFun a self.toFun b

    A SupHom preserves suprema.

    structure InfHom (α : Type u_7) (β : Type u_8) [Min α] [Min β] :
    Type (max u_7 u_8)

    The type of -preserving functions from α to β.

    • toFun : αβ

      The underlying function of an InfHom

    • map_inf' : ∀ (a b : α), self.toFun (a b) = self.toFun a self.toFun b

      An InfHom preserves infima.

    Instances For
      theorem InfHom.map_inf' {α : Type u_7} {β : Type u_8} [Min α] [Min β] (self : InfHom α β) (a : α) (b : α) :
      self.toFun (a b) = self.toFun a self.toFun b

      An InfHom preserves infima.

      structure SupBotHom (α : Type u_7) (β : Type u_8) [Max α] [Max β] [Bot α] [Bot β] extends SupHom :
      Type (max u_7 u_8)

      The type of finitary supremum-preserving homomorphisms from α to β.

      • toFun : αβ
      • map_sup' : ∀ (a b : α), self.toFun (a b) = self.toFun a self.toFun b
      • map_bot' : self.toFun =

        A SupBotHom preserves the bottom element.

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

        A SupBotHom preserves the bottom element.

        structure InfTopHom (α : Type u_7) (β : Type u_8) [Min α] [Min β] [Top α] [Top β] extends InfHom :
        Type (max u_7 u_8)

        The type of finitary infimum-preserving homomorphisms from α to β.

        • toFun : αβ
        • map_inf' : ∀ (a b : α), self.toFun (a b) = self.toFun a self.toFun b
        • map_top' : self.toFun =

          An InfTopHom preserves the top element.

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

          An InfTopHom preserves the top element.

          structure LatticeHom (α : Type u_7) (β : Type u_8) [Lattice α] [Lattice β] extends SupHom :
          Type (max u_7 u_8)

          The type of lattice homomorphisms from α to β.

          • toFun : αβ
          • map_sup' : ∀ (a b : α), self.toFun (a b) = self.toFun a self.toFun b
          • map_inf' : ∀ (a b : α), self.toFun (a b) = self.toFun a self.toFun b

            A LatticeHom preserves infima.

          Instances For
            theorem LatticeHom.map_inf' {α : Type u_7} {β : Type u_8} [Lattice α] [Lattice β] (self : LatticeHom α β) (a : α) (b : α) :
            self.toFun (a b) = self.toFun a self.toFun b

            A LatticeHom preserves infima.

            structure BoundedLatticeHom (α : Type u_7) (β : Type u_8) [Lattice α] [Lattice β] [BoundedOrder α] [BoundedOrder β] extends LatticeHom , SupHom :
            Type (max u_7 u_8)

            The type of bounded lattice homomorphisms from α to β.

            • toFun : αβ
            • map_sup' : ∀ (a b : α), self.toFun (a b) = self.toFun a self.toFun b
            • map_inf' : ∀ (a b : α), self.toFun (a b) = self.toFun a self.toFun b
            • map_top' : self.toFun =

              A BoundedLatticeHom preserves the top element.

            • map_bot' : self.toFun =

              A BoundedLatticeHom preserves the bottom element.

            Instances For
              theorem BoundedLatticeHom.map_top' {α : Type u_7} {β : Type u_8} [Lattice α] [Lattice β] [BoundedOrder α] [BoundedOrder β] (self : BoundedLatticeHom α β) :
              self.toFun =

              A BoundedLatticeHom preserves the top element.

              theorem BoundedLatticeHom.map_bot' {α : Type u_7} {β : Type u_8} [Lattice α] [Lattice β] [BoundedOrder α] [BoundedOrder β] (self : BoundedLatticeHom α β) :
              self.toFun =

              A BoundedLatticeHom preserves the bottom element.

              class SupHomClass (F : Type u_7) (α : Type u_8) (β : Type u_9) [Max α] [Max β] [FunLike F α β] :

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

              You should extend this class when you extend SupHom.

              • map_sup : ∀ (f : F) (a b : α), f (a b) = f a f b

                A SupHomClass morphism preserves suprema.

              Instances
                @[simp]
                theorem SupHomClass.map_sup {F : Type u_7} {α : Type u_8} {β : Type u_9} :
                ∀ {inst : Max α} {inst_1 : Max β} {inst_2 : FunLike F α β} [self : SupHomClass F α β] (f : F) (a b : α), f (a b) = f a f b

                A SupHomClass morphism preserves suprema.

                class InfHomClass (F : Type u_7) (α : Type u_8) (β : Type u_9) [Min α] [Min β] [FunLike F α β] :

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

                You should extend this class when you extend InfHom.

                • map_inf : ∀ (f : F) (a b : α), f (a b) = f a f b

                  An InfHomClass morphism preserves infima.

                Instances
                  @[simp]
                  theorem InfHomClass.map_inf {F : Type u_7} {α : Type u_8} {β : Type u_9} :
                  ∀ {inst : Min α} {inst_1 : Min β} {inst_2 : FunLike F α β} [self : InfHomClass F α β] (f : F) (a b : α), f (a b) = f a f b

                  An InfHomClass morphism preserves infima.

                  class SupBotHomClass (F : Type u_7) (α : Type u_8) (β : Type u_9) [Max α] [Max β] [Bot α] [Bot β] [FunLike F α β] extends SupHomClass :

                  SupBotHomClass F α β states that F is a type of finitary supremum-preserving morphisms.

                  You should extend this class when you extend SupBotHom.

                  • map_sup : ∀ (f : F) (a b : α), f (a b) = f a f b
                  • map_bot : ∀ (f : F), f =

                    A SupBotHomClass morphism preserves the bottom element.

                  Instances
                    theorem SupBotHomClass.map_bot {F : Type u_7} {α : Type u_8} {β : Type u_9} :
                    ∀ {inst : Max α} {inst_1 : Max β} {inst_2 : Bot α} {inst_3 : Bot β} {inst_4 : FunLike F α β} [self : SupBotHomClass F α β] (f : F), f =

                    A SupBotHomClass morphism preserves the bottom element.

                    class InfTopHomClass (F : Type u_7) (α : Type u_8) (β : Type u_9) [Min α] [Min β] [Top α] [Top β] [FunLike F α β] extends InfHomClass :

                    InfTopHomClass F α β states that F is a type of finitary infimum-preserving morphisms.

                    You should extend this class when you extend SupBotHom.

                    • map_inf : ∀ (f : F) (a b : α), f (a b) = f a f b
                    • map_top : ∀ (f : F), f =

                      An InfTopHomClass morphism preserves the top element.

                    Instances
                      theorem InfTopHomClass.map_top {F : Type u_7} {α : Type u_8} {β : Type u_9} :
                      ∀ {inst : Min α} {inst_1 : Min β} {inst_2 : Top α} {inst_3 : Top β} {inst_4 : FunLike F α β} [self : InfTopHomClass F α β] (f : F), f =

                      An InfTopHomClass morphism preserves the top element.

                      class LatticeHomClass (F : Type u_7) (α : Type u_8) (β : Type u_9) [Lattice α] [Lattice β] [FunLike F α β] extends SupHomClass :

                      LatticeHomClass F α β states that F is a type of lattice morphisms.

                      You should extend this class when you extend LatticeHom.

                      • map_sup : ∀ (f : F) (a b : α), f (a b) = f a f b
                      • map_inf : ∀ (f : F) (a b : α), f (a b) = f a f b

                        A LatticeHomClass morphism preserves infima.

                      Instances
                        theorem LatticeHomClass.map_inf {F : Type u_7} {α : Type u_8} {β : Type u_9} :
                        ∀ {inst : Lattice α} {inst_1 : Lattice β} {inst_2 : FunLike F α β} [self : LatticeHomClass F α β] (f : F) (a b : α), f (a b) = f a f b

                        A LatticeHomClass morphism preserves infima.

                        class BoundedLatticeHomClass (F : Type u_7) (α : Type u_8) (β : Type u_9) [Lattice α] [Lattice β] [BoundedOrder α] [BoundedOrder β] [FunLike F α β] extends LatticeHomClass , SupHomClass :

                        BoundedLatticeHomClass F α β states that F is a type of bounded lattice morphisms.

                        You should extend this class when you extend BoundedLatticeHom.

                        Instances
                          theorem BoundedLatticeHomClass.map_top {F : Type u_7} {α : Type u_8} {β : Type u_9} :
                          ∀ {inst : Lattice α} {inst_1 : Lattice β} {inst_2 : BoundedOrder α} {inst_3 : BoundedOrder β} {inst_4 : FunLike F α β} [self : BoundedLatticeHomClass F α β] (f : F), f =

                          A BoundedLatticeHomClass morphism preserves the top element.

                          theorem BoundedLatticeHomClass.map_bot {F : Type u_7} {α : Type u_8} {β : Type u_9} :
                          ∀ {inst : Lattice α} {inst_1 : Lattice β} {inst_2 : BoundedOrder α} {inst_3 : BoundedOrder β} {inst_4 : FunLike F α β} [self : BoundedLatticeHomClass F α β] (f : F), f =

                          A BoundedLatticeHomClass morphism preserves the bottom element.

                          @[instance 100]
                          instance SupHomClass.toOrderHomClass {F : Type u_1} {α : Type u_3} {β : Type u_4} [FunLike F α β] [SemilatticeSup α] [SemilatticeSup β] [SupHomClass F α β] :
                          Equations
                          • =
                          @[instance 100]
                          instance InfHomClass.toOrderHomClass {F : Type u_1} {α : Type u_3} {β : Type u_4} [FunLike F α β] [SemilatticeInf α] [SemilatticeInf β] [InfHomClass F α β] :
                          Equations
                          • =
                          @[instance 100]
                          instance SupBotHomClass.toBotHomClass {F : Type u_1} {α : Type u_3} {β : Type u_4} [FunLike F α β] [Max α] [Max β] [Bot α] [Bot β] [SupBotHomClass F α β] :
                          BotHomClass F α β
                          Equations
                          • =
                          @[instance 100]
                          instance InfTopHomClass.toTopHomClass {F : Type u_1} {α : Type u_3} {β : Type u_4} [FunLike F α β] [Min α] [Min β] [Top α] [Top β] [InfTopHomClass F α β] :
                          TopHomClass F α β
                          Equations
                          • =
                          @[instance 100]
                          instance LatticeHomClass.toInfHomClass {F : Type u_1} {α : Type u_3} {β : Type u_4} [FunLike F α β] [Lattice α] [Lattice β] [LatticeHomClass F α β] :
                          InfHomClass F α β
                          Equations
                          • =
                          @[instance 100]
                          instance BoundedLatticeHomClass.toSupBotHomClass {F : Type u_1} {α : Type u_3} {β : Type u_4} [FunLike F α β] [Lattice α] [Lattice β] [BoundedOrder α] [BoundedOrder β] [BoundedLatticeHomClass F α β] :
                          Equations
                          • =
                          @[instance 100]
                          instance BoundedLatticeHomClass.toInfTopHomClass {F : Type u_1} {α : Type u_3} {β : Type u_4} [FunLike F α β] [Lattice α] [Lattice β] [BoundedOrder α] [BoundedOrder β] [BoundedLatticeHomClass F α β] :
                          Equations
                          • =
                          @[instance 100]
                          instance BoundedLatticeHomClass.toBoundedOrderHomClass {F : Type u_1} {α : Type u_3} {β : Type u_4} [FunLike F α β] [Lattice α] [Lattice β] [BoundedOrder α] [BoundedOrder β] [BoundedLatticeHomClass F α β] :
                          Equations
                          • =
                          @[instance 100]
                          instance OrderIsoClass.toSupHomClass {F : Type u_1} {α : Type u_3} {β : Type u_4} [EquivLike F α β] [SemilatticeSup α] [SemilatticeSup β] [OrderIsoClass F α β] :
                          SupHomClass F α β
                          Equations
                          • =
                          @[instance 100]
                          instance OrderIsoClass.toInfHomClass {F : Type u_1} {α : Type u_3} {β : Type u_4} [EquivLike F α β] [SemilatticeInf α] [SemilatticeInf β] [OrderIsoClass F α β] :
                          InfHomClass F α β
                          Equations
                          • =
                          @[instance 100]
                          instance OrderIsoClass.toSupBotHomClass {F : Type u_1} {α : Type u_3} {β : Type u_4} [EquivLike F α β] [SemilatticeSup α] [OrderBot α] [SemilatticeSup β] [OrderBot β] [OrderIsoClass F α β] :
                          Equations
                          • =
                          @[instance 100]
                          instance OrderIsoClass.toInfTopHomClass {F : Type u_1} {α : Type u_3} {β : Type u_4} [EquivLike F α β] [SemilatticeInf α] [OrderTop α] [SemilatticeInf β] [OrderTop β] [OrderIsoClass F α β] :
                          Equations
                          • =
                          @[instance 100]
                          instance OrderIsoClass.toLatticeHomClass {F : Type u_1} {α : Type u_3} {β : Type u_4} [EquivLike F α β] [Lattice α] [Lattice β] [OrderIsoClass F α β] :
                          Equations
                          • =
                          @[instance 100]
                          instance OrderIsoClass.toBoundedLatticeHomClass {F : Type u_1} {α : Type u_3} {β : Type u_4} [EquivLike F α β] [Lattice α] [Lattice β] [BoundedOrder α] [BoundedOrder β] [OrderIsoClass F α β] :
                          Equations
                          • =
                          def orderEmbeddingOfInjective {F : Type u_1} {α : Type u_3} {β : Type u_4} [FunLike F α β] [SemilatticeInf α] [SemilatticeInf β] (f : F) [InfHomClass F α β] (hf : Function.Injective f) :
                          α ↪o β

                          We can regard an injective map preserving binary infima as an order embedding.

                          Equations
                          Instances For
                            @[simp]
                            theorem orderEmbeddingOfInjective_apply {F : Type u_1} {α : Type u_3} {β : Type u_4} [FunLike F α β] [SemilatticeInf α] [SemilatticeInf β] (f : F) [InfHomClass F α β] (hf : Function.Injective f) (a : α) :
                            theorem Disjoint.map {F : Type u_1} {α : Type u_3} {β : Type u_4} [Lattice α] [BoundedOrder α] [Lattice β] [BoundedOrder β] [FunLike F α β] [BoundedLatticeHomClass F α β] (f : F) {a : α} {b : α} (h : Disjoint a b) :
                            Disjoint (f a) (f b)
                            theorem Codisjoint.map {F : Type u_1} {α : Type u_3} {β : Type u_4} [Lattice α] [BoundedOrder α] [Lattice β] [BoundedOrder β] [FunLike F α β] [BoundedLatticeHomClass F α β] (f : F) {a : α} {b : α} (h : Codisjoint a b) :
                            Codisjoint (f a) (f b)
                            theorem IsCompl.map {F : Type u_1} {α : Type u_3} {β : Type u_4} [Lattice α] [BoundedOrder α] [Lattice β] [BoundedOrder β] [FunLike F α β] [BoundedLatticeHomClass F α β] (f : F) {a : α} {b : α} (h : IsCompl a b) :
                            IsCompl (f a) (f b)
                            theorem map_compl' {F : Type u_1} {α : Type u_3} {β : Type u_4} [BooleanAlgebra α] [BooleanAlgebra β] [FunLike F α β] [BoundedLatticeHomClass F α β] (f : F) (a : α) :
                            f a = (f a)

                            Special case of map_compl for boolean algebras.

                            theorem map_sdiff' {F : Type u_1} {α : Type u_3} {β : Type u_4} [BooleanAlgebra α] [BooleanAlgebra β] [FunLike F α β] [BoundedLatticeHomClass F α β] (f : F) (a : α) (b : α) :
                            f (a \ b) = f a \ f b

                            Special case of map_sdiff for boolean algebras.

                            theorem map_symmDiff' {F : Type u_1} {α : Type u_3} {β : Type u_4} [BooleanAlgebra α] [BooleanAlgebra β] [FunLike F α β] [BoundedLatticeHomClass F α β] (f : F) (a : α) (b : α) :
                            f (symmDiff a b) = symmDiff (f a) (f b)

                            Special case of map_symmDiff for boolean algebras.

                            instance instCoeTCSupHomOfSupHomClass {F : Type u_1} {α : Type u_3} {β : Type u_4} [FunLike F α β] [Max α] [Max β] [SupHomClass F α β] :
                            CoeTC F (SupHom α β)
                            Equations
                            • instCoeTCSupHomOfSupHomClass = { coe := fun (f : F) => { toFun := f, map_sup' := } }
                            instance instCoeTCInfHomOfInfHomClass {F : Type u_1} {α : Type u_3} {β : Type u_4} [FunLike F α β] [Min α] [Min β] [InfHomClass F α β] :
                            CoeTC F (InfHom α β)
                            Equations
                            • instCoeTCInfHomOfInfHomClass = { coe := fun (f : F) => { toFun := f, map_inf' := } }
                            instance instCoeTCSupBotHomOfSupBotHomClass {F : Type u_1} {α : Type u_3} {β : Type u_4} [FunLike F α β] [Max α] [Max β] [Bot α] [Bot β] [SupBotHomClass F α β] :
                            CoeTC F (SupBotHom α β)
                            Equations
                            • instCoeTCSupBotHomOfSupBotHomClass = { coe := fun (f : F) => { toFun := f, map_sup' := , map_bot' := } }
                            instance instCoeTCInfTopHomOfInfTopHomClass {F : Type u_1} {α : Type u_3} {β : Type u_4} [FunLike F α β] [Min α] [Min β] [Top α] [Top β] [InfTopHomClass F α β] :
                            CoeTC F (InfTopHom α β)
                            Equations
                            • instCoeTCInfTopHomOfInfTopHomClass = { coe := fun (f : F) => { toFun := f, map_inf' := , map_top' := } }
                            instance instCoeTCLatticeHomOfLatticeHomClass {F : Type u_1} {α : Type u_3} {β : Type u_4} [FunLike F α β] [Lattice α] [Lattice β] [LatticeHomClass F α β] :
                            CoeTC F (LatticeHom α β)
                            Equations
                            • instCoeTCLatticeHomOfLatticeHomClass = { coe := fun (f : F) => { toFun := f, map_sup' := , map_inf' := } }
                            instance instCoeTCBoundedLatticeHomOfBoundedLatticeHomClass {F : Type u_1} {α : Type u_3} {β : Type u_4} [FunLike F α β] [Lattice α] [Lattice β] [BoundedOrder α] [BoundedOrder β] [BoundedLatticeHomClass F α β] :
                            Equations
                            • One or more equations did not get rendered due to their size.

                            Supremum homomorphisms #

                            instance SupHom.instFunLike {α : Type u_3} {β : Type u_4} [Max α] [Max β] :
                            FunLike (SupHom α β) α β
                            Equations
                            • SupHom.instFunLike = { coe := SupHom.toFun, coe_injective' := }
                            instance SupHom.instSupHomClass {α : Type u_3} {β : Type u_4} [Max α] [Max β] :
                            SupHomClass (SupHom α β) α β
                            Equations
                            • =
                            @[simp]
                            theorem SupHom.toFun_eq_coe {α : Type u_3} {β : Type u_4} [Max α] [Max β] (f : SupHom α β) :
                            f.toFun = f
                            @[simp]
                            theorem SupHom.coe_mk {α : Type u_3} {β : Type u_4} [Max α] [Max β] (f : αβ) (hf : ∀ (a b : α), f (a b) = f a f b) :
                            { toFun := f, map_sup' := hf } = f
                            theorem SupHom.ext {α : Type u_3} {β : Type u_4} [Max α] [Max β] {f : SupHom α β} {g : SupHom α β} (h : ∀ (a : α), f a = g a) :
                            f = g
                            def SupHom.copy {α : Type u_3} {β : Type u_4} [Max α] [Max β] (f : SupHom α β) (f' : αβ) (h : f' = f) :
                            SupHom α β

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

                            Equations
                            • f.copy f' h = { toFun := f', map_sup' := }
                            Instances For
                              @[simp]
                              theorem SupHom.coe_copy {α : Type u_3} {β : Type u_4} [Max α] [Max β] (f : SupHom α β) (f' : αβ) (h : f' = f) :
                              (f.copy f' h) = f'
                              theorem SupHom.copy_eq {α : Type u_3} {β : Type u_4} [Max α] [Max β] (f : SupHom α β) (f' : αβ) (h : f' = f) :
                              f.copy f' h = f
                              def SupHom.id (α : Type u_3) [Max α] :
                              SupHom α α

                              id as a SupHom.

                              Equations
                              Instances For
                                instance SupHom.instInhabited (α : Type u_3) [Max α] :
                                Equations
                                @[simp]
                                theorem SupHom.coe_id (α : Type u_3) [Max α] :
                                (SupHom.id α) = id
                                @[simp]
                                theorem SupHom.id_apply {α : Type u_3} [Max α] (a : α) :
                                (SupHom.id α) a = a
                                def SupHom.comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Max α] [Max β] [Max γ] (f : SupHom β γ) (g : SupHom α β) :
                                SupHom α γ

                                Composition of SupHoms as a SupHom.

                                Equations
                                • f.comp g = { toFun := f g, map_sup' := }
                                Instances For
                                  @[simp]
                                  theorem SupHom.coe_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Max α] [Max β] [Max γ] (f : SupHom β γ) (g : SupHom α β) :
                                  (f.comp g) = f g
                                  @[simp]
                                  theorem SupHom.comp_apply {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Max α] [Max β] [Max γ] (f : SupHom β γ) (g : SupHom α β) (a : α) :
                                  (f.comp g) a = f (g a)
                                  @[simp]
                                  theorem SupHom.comp_assoc {α : Type u_3} {β : Type u_4} {γ : Type u_5} {δ : Type u_6} [Max α] [Max β] [Max γ] [Max δ] (f : SupHom γ δ) (g : SupHom β γ) (h : SupHom α β) :
                                  (f.comp g).comp h = f.comp (g.comp h)
                                  @[simp]
                                  theorem SupHom.comp_id {α : Type u_3} {β : Type u_4} [Max α] [Max β] (f : SupHom α β) :
                                  f.comp (SupHom.id α) = f
                                  @[simp]
                                  theorem SupHom.id_comp {α : Type u_3} {β : Type u_4} [Max α] [Max β] (f : SupHom α β) :
                                  (SupHom.id β).comp f = f
                                  @[simp]
                                  theorem SupHom.cancel_right {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Max α] [Max β] [Max γ] {g₁ : SupHom β γ} {g₂ : SupHom β γ} {f : SupHom α β} (hf : Function.Surjective f) :
                                  g₁.comp f = g₂.comp f g₁ = g₂
                                  @[simp]
                                  theorem SupHom.cancel_left {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Max α] [Max β] [Max γ] {g : SupHom β γ} {f₁ : SupHom α β} {f₂ : SupHom α β} (hg : Function.Injective g) :
                                  g.comp f₁ = g.comp f₂ f₁ = f₂
                                  def SupHom.const (α : Type u_3) {β : Type u_4} [Max α] [SemilatticeSup β] (b : β) :
                                  SupHom α β

                                  The constant function as a SupHom.

                                  Equations
                                  • SupHom.const α b = { toFun := fun (x : α) => b, map_sup' := }
                                  Instances For
                                    @[simp]
                                    theorem SupHom.coe_const (α : Type u_3) {β : Type u_4} [Max α] [SemilatticeSup β] (b : β) :
                                    @[simp]
                                    theorem SupHom.const_apply (α : Type u_3) {β : Type u_4} [Max α] [SemilatticeSup β] (b : β) (a : α) :
                                    (SupHom.const α b) a = b
                                    instance SupHom.instMax {α : Type u_3} {β : Type u_4} [Max α] [SemilatticeSup β] :
                                    Max (SupHom α β)
                                    Equations
                                    • SupHom.instMax = { max := fun (f g : SupHom α β) => { toFun := f g, map_sup' := } }
                                    instance SupHom.instSemilatticeSup {α : Type u_3} {β : Type u_4} [Max α] [SemilatticeSup β] :
                                    Equations
                                    instance SupHom.instBot {α : Type u_3} {β : Type u_4} [Max α] [SemilatticeSup β] [Bot β] :
                                    Bot (SupHom α β)
                                    Equations
                                    instance SupHom.instTop {α : Type u_3} {β : Type u_4} [Max α] [SemilatticeSup β] [Top β] :
                                    Top (SupHom α β)
                                    Equations
                                    instance SupHom.instOrderBot {α : Type u_3} {β : Type u_4} [Max α] [SemilatticeSup β] [OrderBot β] :
                                    Equations
                                    instance SupHom.instOrderTop {α : Type u_3} {β : Type u_4} [Max α] [SemilatticeSup β] [OrderTop β] :
                                    Equations
                                    instance SupHom.instBoundedOrder {α : Type u_3} {β : Type u_4} [Max α] [SemilatticeSup β] [BoundedOrder β] :
                                    Equations
                                    @[simp]
                                    theorem SupHom.coe_sup {α : Type u_3} {β : Type u_4} [Max α] [SemilatticeSup β] (f : SupHom α β) (g : SupHom α β) :
                                    (f g) = (f g)
                                    @[simp]
                                    theorem SupHom.coe_bot {α : Type u_3} {β : Type u_4} [Max α] [SemilatticeSup β] [Bot β] :
                                    =
                                    @[simp]
                                    theorem SupHom.coe_top {α : Type u_3} {β : Type u_4} [Max α] [SemilatticeSup β] [Top β] :
                                    =
                                    @[simp]
                                    theorem SupHom.sup_apply {α : Type u_3} {β : Type u_4} [Max α] [SemilatticeSup β] (f : SupHom α β) (g : SupHom α β) (a : α) :
                                    (f g) a = f a g a
                                    @[simp]
                                    theorem SupHom.bot_apply {α : Type u_3} {β : Type u_4} [Max α] [SemilatticeSup β] [Bot β] (a : α) :
                                    @[simp]
                                    theorem SupHom.top_apply {α : Type u_3} {β : Type u_4} [Max α] [SemilatticeSup β] [Top β] (a : α) :
                                    def SupHom.subtypeVal {β : Type u_4} [SemilatticeSup β] {P : βProp} (Psup : ∀ ⦃x y : β⦄, P xP yP (x y)) :
                                    SupHom { x : β // P x } β

                                    Subtype.val as a SupHom.

                                    Equations
                                    Instances For
                                      @[simp]
                                      theorem SupHom.subtypeVal_apply {β : Type u_4} [SemilatticeSup β] {P : βProp} (Psup : ∀ ⦃x y : β⦄, P xP yP (x y)) (x : { x : β // P x }) :
                                      (SupHom.subtypeVal Psup) x = x
                                      @[simp]
                                      theorem SupHom.subtypeVal_coe {β : Type u_4} [SemilatticeSup β] {P : βProp} (Psup : ∀ ⦃x y : β⦄, P xP yP (x y)) :
                                      (SupHom.subtypeVal Psup) = Subtype.val

                                      Infimum homomorphisms #

                                      instance InfHom.instFunLike {α : Type u_3} {β : Type u_4} [Min α] [Min β] :
                                      FunLike (InfHom α β) α β
                                      Equations
                                      • InfHom.instFunLike = { coe := InfHom.toFun, coe_injective' := }
                                      instance InfHom.instInfHomClass {α : Type u_3} {β : Type u_4} [Min α] [Min β] :
                                      InfHomClass (InfHom α β) α β
                                      Equations
                                      • =
                                      @[simp]
                                      theorem InfHom.toFun_eq_coe {α : Type u_3} {β : Type u_4} [Min α] [Min β] (f : InfHom α β) :
                                      f.toFun = f
                                      @[simp]
                                      theorem InfHom.coe_mk {α : Type u_3} {β : Type u_4} [Min α] [Min β] (f : αβ) (hf : ∀ (a b : α), f (a b) = f a f b) :
                                      { toFun := f, map_inf' := hf } = f
                                      theorem InfHom.ext {α : Type u_3} {β : Type u_4} [Min α] [Min β] {f : InfHom α β} {g : InfHom α β} (h : ∀ (a : α), f a = g a) :
                                      f = g
                                      def InfHom.copy {α : Type u_3} {β : Type u_4} [Min α] [Min β] (f : InfHom α β) (f' : αβ) (h : f' = f) :
                                      InfHom α β

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

                                      Equations
                                      • f.copy f' h = { toFun := f', map_inf' := }
                                      Instances For
                                        @[simp]
                                        theorem InfHom.coe_copy {α : Type u_3} {β : Type u_4} [Min α] [Min β] (f : InfHom α β) (f' : αβ) (h : f' = f) :
                                        (f.copy f' h) = f'
                                        theorem InfHom.copy_eq {α : Type u_3} {β : Type u_4} [Min α] [Min β] (f : InfHom α β) (f' : αβ) (h : f' = f) :
                                        f.copy f' h = f
                                        def InfHom.id (α : Type u_3) [Min α] :
                                        InfHom α α

                                        id as an InfHom.

                                        Equations
                                        Instances For
                                          instance InfHom.instInhabited (α : Type u_3) [Min α] :
                                          Equations
                                          @[simp]
                                          theorem InfHom.coe_id (α : Type u_3) [Min α] :
                                          (InfHom.id α) = id
                                          @[simp]
                                          theorem InfHom.id_apply {α : Type u_3} [Min α] (a : α) :
                                          (InfHom.id α) a = a
                                          def InfHom.comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Min α] [Min β] [Min γ] (f : InfHom β γ) (g : InfHom α β) :
                                          InfHom α γ

                                          Composition of InfHoms as an InfHom.

                                          Equations
                                          • f.comp g = { toFun := f g, map_inf' := }
                                          Instances For
                                            @[simp]
                                            theorem InfHom.coe_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Min α] [Min β] [Min γ] (f : InfHom β γ) (g : InfHom α β) :
                                            (f.comp g) = f g
                                            @[simp]
                                            theorem InfHom.comp_apply {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Min α] [Min β] [Min γ] (f : InfHom β γ) (g : InfHom α β) (a : α) :
                                            (f.comp g) a = f (g a)
                                            @[simp]
                                            theorem InfHom.comp_assoc {α : Type u_3} {β : Type u_4} {γ : Type u_5} {δ : Type u_6} [Min α] [Min β] [Min γ] [Min δ] (f : InfHom γ δ) (g : InfHom β γ) (h : InfHom α β) :
                                            (f.comp g).comp h = f.comp (g.comp h)
                                            @[simp]
                                            theorem InfHom.comp_id {α : Type u_3} {β : Type u_4} [Min α] [Min β] (f : InfHom α β) :
                                            f.comp (InfHom.id α) = f
                                            @[simp]
                                            theorem InfHom.id_comp {α : Type u_3} {β : Type u_4} [Min α] [Min β] (f : InfHom α β) :
                                            (InfHom.id β).comp f = f
                                            @[simp]
                                            theorem InfHom.cancel_right {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Min α] [Min β] [Min γ] {g₁ : InfHom β γ} {g₂ : InfHom β γ} {f : InfHom α β} (hf : Function.Surjective f) :
                                            g₁.comp f = g₂.comp f g₁ = g₂
                                            @[simp]
                                            theorem InfHom.cancel_left {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Min α] [Min β] [Min γ] {g : InfHom β γ} {f₁ : InfHom α β} {f₂ : InfHom α β} (hg : Function.Injective g) :
                                            g.comp f₁ = g.comp f₂ f₁ = f₂
                                            def InfHom.const (α : Type u_3) {β : Type u_4} [Min α] [SemilatticeInf β] (b : β) :
                                            InfHom α β

                                            The constant function as an InfHom.

                                            Equations
                                            • InfHom.const α b = { toFun := fun (x : α) => b, map_inf' := }
                                            Instances For
                                              @[simp]
                                              theorem InfHom.coe_const (α : Type u_3) {β : Type u_4} [Min α] [SemilatticeInf β] (b : β) :
                                              @[simp]
                                              theorem InfHom.const_apply (α : Type u_3) {β : Type u_4} [Min α] [SemilatticeInf β] (b : β) (a : α) :
                                              (InfHom.const α b) a = b
                                              instance InfHom.instMin {α : Type u_3} {β : Type u_4} [Min α] [SemilatticeInf β] :
                                              Min (InfHom α β)
                                              Equations
                                              • InfHom.instMin = { min := fun (f g : InfHom α β) => { toFun := f g, map_inf' := } }
                                              instance InfHom.instSemilatticeInf {α : Type u_3} {β : Type u_4} [Min α] [SemilatticeInf β] :
                                              Equations
                                              instance InfHom.instBot {α : Type u_3} {β : Type u_4} [Min α] [SemilatticeInf β] [Bot β] :
                                              Bot (InfHom α β)
                                              Equations
                                              instance InfHom.instTop {α : Type u_3} {β : Type u_4} [Min α] [SemilatticeInf β] [Top β] :
                                              Top (InfHom α β)
                                              Equations
                                              instance InfHom.instOrderBot {α : Type u_3} {β : Type u_4} [Min α] [SemilatticeInf β] [OrderBot β] :
                                              Equations
                                              instance InfHom.instOrderTop {α : Type u_3} {β : Type u_4} [Min α] [SemilatticeInf β] [OrderTop β] :
                                              Equations
                                              instance InfHom.instBoundedOrder {α : Type u_3} {β : Type u_4} [Min α] [SemilatticeInf β] [BoundedOrder β] :
                                              Equations
                                              @[simp]
                                              theorem InfHom.coe_inf {α : Type u_3} {β : Type u_4} [Min α] [SemilatticeInf β] (f : InfHom α β) (g : InfHom α β) :
                                              (f g) = (f g)
                                              @[simp]
                                              theorem InfHom.coe_bot {α : Type u_3} {β : Type u_4} [Min α] [SemilatticeInf β] [Bot β] :
                                              =
                                              @[simp]
                                              theorem InfHom.coe_top {α : Type u_3} {β : Type u_4} [Min α] [SemilatticeInf β] [Top β] :
                                              =
                                              @[simp]
                                              theorem InfHom.inf_apply {α : Type u_3} {β : Type u_4} [Min α] [SemilatticeInf β] (f : InfHom α β) (g : InfHom α β) (a : α) :
                                              (f g) a = f a g a
                                              @[simp]
                                              theorem InfHom.bot_apply {α : Type u_3} {β : Type u_4} [Min α] [SemilatticeInf β] [Bot β] (a : α) :
                                              @[simp]
                                              theorem InfHom.top_apply {α : Type u_3} {β : Type u_4} [Min α] [SemilatticeInf β] [Top β] (a : α) :
                                              def InfHom.subtypeVal {β : Type u_4} [SemilatticeInf β] {P : βProp} (Pinf : ∀ ⦃x y : β⦄, P xP yP (x y)) :
                                              InfHom { x : β // P x } β

                                              Subtype.val as an InfHom.

                                              Equations
                                              Instances For
                                                @[simp]
                                                theorem InfHom.subtypeVal_apply {β : Type u_4} [SemilatticeInf β] {P : βProp} (Pinf : ∀ ⦃x y : β⦄, P xP yP (x y)) (x : { x : β // P x }) :
                                                (InfHom.subtypeVal Pinf) x = x
                                                @[simp]
                                                theorem InfHom.subtypeVal_coe {β : Type u_4} [SemilatticeInf β] {P : βProp} (Pinf : ∀ ⦃x y : β⦄, P xP yP (x y)) :
                                                (InfHom.subtypeVal Pinf) = Subtype.val

                                                Finitary supremum homomorphisms #

                                                def SupBotHom.toBotHom {α : Type u_3} {β : Type u_4} [Max α] [Bot α] [Max β] [Bot β] (f : SupBotHom α β) :
                                                BotHom α β

                                                Reinterpret a SupBotHom as a BotHom.

                                                Equations
                                                • f.toBotHom = { toFun := f.toFun, map_bot' := }
                                                Instances For
                                                  instance SupBotHom.instFunLike {α : Type u_3} {β : Type u_4} [Max α] [Bot α] [Max β] [Bot β] :
                                                  FunLike (SupBotHom α β) α β
                                                  Equations
                                                  • SupBotHom.instFunLike = { coe := fun (f : SupBotHom α β) => f.toFun, coe_injective' := }
                                                  instance SupBotHom.instSupBotHomClass {α : Type u_3} {β : Type u_4} [Max α] [Bot α] [Max β] [Bot β] :
                                                  Equations
                                                  • =
                                                  theorem SupBotHom.toFun_eq_coe {α : Type u_3} {β : Type u_4} [Max α] [Bot α] [Max β] [Bot β] (f : SupBotHom α β) :
                                                  f.toFun = f
                                                  @[simp]
                                                  theorem SupBotHom.coe_toSupHom {α : Type u_3} {β : Type u_4} [Max α] [Bot α] [Max β] [Bot β] (f : SupBotHom α β) :
                                                  f.toSupHom = f
                                                  @[simp]
                                                  theorem SupBotHom.coe_toBotHom {α : Type u_3} {β : Type u_4} [Max α] [Bot α] [Max β] [Bot β] (f : SupBotHom α β) :
                                                  f.toBotHom = f
                                                  @[simp]
                                                  theorem SupBotHom.coe_mk {α : Type u_3} {β : Type u_4} [Max α] [Bot α] [Max β] [Bot β] (f : SupHom α β) (hf : f.toFun = ) :
                                                  { toSupHom := f, map_bot' := hf } = f
                                                  theorem SupBotHom.ext {α : Type u_3} {β : Type u_4} [Max α] [Bot α] [Max β] [Bot β] {f : SupBotHom α β} {g : SupBotHom α β} (h : ∀ (a : α), f a = g a) :
                                                  f = g
                                                  def SupBotHom.copy {α : Type u_3} {β : Type u_4} [Max α] [Bot α] [Max β] [Bot β] (f : SupBotHom α β) (f' : αβ) (h : f' = f) :
                                                  SupBotHom α β

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

                                                  Equations
                                                  • f.copy f' h = { toSupHom := f.copy f' h, map_bot' := }
                                                  Instances For
                                                    @[simp]
                                                    theorem SupBotHom.coe_copy {α : Type u_3} {β : Type u_4} [Max α] [Bot α] [Max β] [Bot β] (f : SupBotHom α β) (f' : αβ) (h : f' = f) :
                                                    (f.copy f' h) = f'
                                                    theorem SupBotHom.copy_eq {α : Type u_3} {β : Type u_4} [Max α] [Bot α] [Max β] [Bot β] (f : SupBotHom α β) (f' : αβ) (h : f' = f) :
                                                    f.copy f' h = f
                                                    def SupBotHom.id (α : Type u_3) [Max α] [Bot α] :
                                                    SupBotHom α α

                                                    id as a SupBotHom.

                                                    Equations
                                                    Instances For
                                                      @[simp]
                                                      theorem SupBotHom.id_toSupHom (α : Type u_3) [Max α] [Bot α] :
                                                      (SupBotHom.id α).toSupHom = SupHom.id α
                                                      instance SupBotHom.instInhabited (α : Type u_3) [Max α] [Bot α] :
                                                      Equations
                                                      @[simp]
                                                      theorem SupBotHom.coe_id (α : Type u_3) [Max α] [Bot α] :
                                                      (SupBotHom.id α) = id
                                                      @[simp]
                                                      theorem SupBotHom.id_apply {α : Type u_3} [Max α] [Bot α] (a : α) :
                                                      (SupBotHom.id α) a = a
                                                      def SupBotHom.comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Max α] [Bot α] [Max β] [Bot β] [Max γ] [Bot γ] (f : SupBotHom β γ) (g : SupBotHom α β) :
                                                      SupBotHom α γ

                                                      Composition of SupBotHoms as a SupBotHom.

                                                      Equations
                                                      • f.comp g = { toSupHom := f.comp g.toSupHom, map_bot' := }
                                                      Instances For
                                                        @[simp]
                                                        theorem SupBotHom.coe_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Max α] [Bot α] [Max β] [Bot β] [Max γ] [Bot γ] (f : SupBotHom β γ) (g : SupBotHom α β) :
                                                        (f.comp g) = f g
                                                        @[simp]
                                                        theorem SupBotHom.comp_apply {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Max α] [Bot α] [Max β] [Bot β] [Max γ] [Bot γ] (f : SupBotHom β γ) (g : SupBotHom α β) (a : α) :
                                                        (f.comp g) a = f (g a)
                                                        @[simp]
                                                        theorem SupBotHom.comp_assoc {α : Type u_3} {β : Type u_4} {γ : Type u_5} {δ : Type u_6} [Max α] [Bot α] [Max β] [Bot β] [Max γ] [Bot γ] [Max δ] [Bot δ] (f : SupBotHom γ δ) (g : SupBotHom β γ) (h : SupBotHom α β) :
                                                        (f.comp g).comp h = f.comp (g.comp h)
                                                        @[simp]
                                                        theorem SupBotHom.comp_id {α : Type u_3} {β : Type u_4} [Max α] [Bot α] [Max β] [Bot β] (f : SupBotHom α β) :
                                                        f.comp (SupBotHom.id α) = f
                                                        @[simp]
                                                        theorem SupBotHom.id_comp {α : Type u_3} {β : Type u_4} [Max α] [Bot α] [Max β] [Bot β] (f : SupBotHom α β) :
                                                        (SupBotHom.id β).comp f = f
                                                        @[simp]
                                                        theorem SupBotHom.cancel_right {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Max α] [Bot α] [Max β] [Bot β] [Max γ] [Bot γ] {g₁ : SupBotHom β γ} {g₂ : SupBotHom β γ} {f : SupBotHom α β} (hf : Function.Surjective f) :
                                                        g₁.comp f = g₂.comp f g₁ = g₂
                                                        @[simp]
                                                        theorem SupBotHom.cancel_left {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Max α] [Bot α] [Max β] [Bot β] [Max γ] [Bot γ] {g : SupBotHom β γ} {f₁ : SupBotHom α β} {f₂ : SupBotHom α β} (hg : Function.Injective g) :
                                                        g.comp f₁ = g.comp f₂ f₁ = f₂
                                                        instance SupBotHom.instMax {α : Type u_3} {β : Type u_4} [Max α] [Bot α] [SemilatticeSup β] [OrderBot β] :
                                                        Max (SupBotHom α β)
                                                        Equations
                                                        • SupBotHom.instMax = { max := fun (f g : SupBotHom α β) => let __src := f.toBotHom g.toBotHom; { toSupHom := f.toSupHom g.toSupHom, map_bot' := } }
                                                        instance SupBotHom.instSemilatticeSup {α : Type u_3} {β : Type u_4} [Max α] [Bot α] [SemilatticeSup β] [OrderBot β] :
                                                        Equations
                                                        instance SupBotHom.instOrderBot {α : Type u_3} {β : Type u_4} [Max α] [Bot α] [SemilatticeSup β] [OrderBot β] :
                                                        Equations
                                                        @[simp]
                                                        theorem SupBotHom.coe_sup {α : Type u_3} {β : Type u_4} [Max α] [Bot α] [SemilatticeSup β] [OrderBot β] (f : SupBotHom α β) (g : SupBotHom α β) :
                                                        (f g) = (f g)
                                                        @[simp]
                                                        theorem SupBotHom.coe_bot {α : Type u_3} {β : Type u_4} [Max α] [Bot α] [SemilatticeSup β] [OrderBot β] :
                                                        =
                                                        @[simp]
                                                        theorem SupBotHom.sup_apply {α : Type u_3} {β : Type u_4} [Max α] [Bot α] [SemilatticeSup β] [OrderBot β] (f : SupBotHom α β) (g : SupBotHom α β) (a : α) :
                                                        (f g) a = f a g a
                                                        @[simp]
                                                        theorem SupBotHom.bot_apply {α : Type u_3} {β : Type u_4} [Max α] [Bot α] [SemilatticeSup β] [OrderBot β] (a : α) :
                                                        def SupBotHom.subtypeVal {β : Type u_4} [SemilatticeSup β] [OrderBot β] {P : βProp} (Pbot : P ) (Psup : ∀ ⦃x y : β⦄, P xP yP (x y)) :
                                                        SupBotHom { x : β // P x } β

                                                        Subtype.val as a SupBotHom.

                                                        Equations
                                                        Instances For
                                                          @[simp]
                                                          theorem SupBotHom.subtypeVal_apply {β : Type u_4} [SemilatticeSup β] [OrderBot β] {P : βProp} (Pbot : P ) (Psup : ∀ ⦃x y : β⦄, P xP yP (x y)) (x : { x : β // P x }) :
                                                          (SupBotHom.subtypeVal Pbot Psup) x = x
                                                          @[simp]
                                                          theorem SupBotHom.subtypeVal_coe {β : Type u_4} [SemilatticeSup β] [OrderBot β] {P : βProp} (Pbot : P ) (Psup : ∀ ⦃x y : β⦄, P xP yP (x y)) :
                                                          (SupBotHom.subtypeVal Pbot Psup) = Subtype.val

                                                          Finitary infimum homomorphisms #

                                                          def InfTopHom.toTopHom {α : Type u_3} {β : Type u_4} [Min α] [Top α] [Min β] [Top β] (f : InfTopHom α β) :
                                                          TopHom α β

                                                          Reinterpret an InfTopHom as a TopHom.

                                                          Equations
                                                          • f.toTopHom = { toFun := f.toFun, map_top' := }
                                                          Instances For
                                                            instance InfTopHom.instFunLike {α : Type u_3} {β : Type u_4} [Min α] [Top α] [Min β] [Top β] :
                                                            FunLike (InfTopHom α β) α β
                                                            Equations
                                                            • InfTopHom.instFunLike = { coe := fun (f : InfTopHom α β) => f.toFun, coe_injective' := }
                                                            instance InfTopHom.instInfTopHomClass {α : Type u_3} {β : Type u_4} [Min α] [Top α] [Min β] [Top β] :
                                                            Equations
                                                            • =
                                                            theorem InfTopHom.toFun_eq_coe {α : Type u_3} {β : Type u_4} [Min α] [Top α] [Min β] [Top β] (f : InfTopHom α β) :
                                                            f.toFun = f
                                                            @[simp]
                                                            theorem InfTopHom.coe_toInfHom {α : Type u_3} {β : Type u_4} [Min α] [Top α] [Min β] [Top β] (f : InfTopHom α β) :
                                                            f.toInfHom = f
                                                            @[simp]
                                                            theorem InfTopHom.coe_toTopHom {α : Type u_3} {β : Type u_4} [Min α] [Top α] [Min β] [Top β] (f : InfTopHom α β) :
                                                            f.toTopHom = f
                                                            @[simp]
                                                            theorem InfTopHom.coe_mk {α : Type u_3} {β : Type u_4} [Min α] [Top α] [Min β] [Top β] (f : InfHom α β) (hf : f.toFun = ) :
                                                            { toInfHom := f, map_top' := hf } = f
                                                            theorem InfTopHom.ext {α : Type u_3} {β : Type u_4} [Min α] [Top α] [Min β] [Top β] {f : InfTopHom α β} {g : InfTopHom α β} (h : ∀ (a : α), f a = g a) :
                                                            f = g
                                                            def InfTopHom.copy {α : Type u_3} {β : Type u_4} [Min α] [Top α] [Min β] [Top β] (f : InfTopHom α β) (f' : αβ) (h : f' = f) :
                                                            InfTopHom α β

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

                                                            Equations
                                                            • f.copy f' h = { toInfHom := f.copy f' h, map_top' := }
                                                            Instances For
                                                              @[simp]
                                                              theorem InfTopHom.coe_copy {α : Type u_3} {β : Type u_4} [Min α] [Top α] [Min β] [Top β] (f : InfTopHom α β) (f' : αβ) (h : f' = f) :
                                                              (f.copy f' h) = f'
                                                              theorem InfTopHom.copy_eq {α : Type u_3} {β : Type u_4} [Min α] [Top α] [Min β] [Top β] (f : InfTopHom α β) (f' : αβ) (h : f' = f) :
                                                              f.copy f' h = f
                                                              def InfTopHom.id (α : Type u_3) [Min α] [Top α] :
                                                              InfTopHom α α

                                                              id as an InfTopHom.

                                                              Equations
                                                              Instances For
                                                                @[simp]
                                                                theorem InfTopHom.id_toInfHom (α : Type u_3) [Min α] [Top α] :
                                                                (InfTopHom.id α).toInfHom = InfHom.id α
                                                                instance InfTopHom.instInhabited (α : Type u_3) [Min α] [Top α] :
                                                                Equations
                                                                @[simp]
                                                                theorem InfTopHom.coe_id (α : Type u_3) [Min α] [Top α] :
                                                                (InfTopHom.id α) = id
                                                                @[simp]
                                                                theorem InfTopHom.id_apply {α : Type u_3} [Min α] [Top α] (a : α) :
                                                                (InfTopHom.id α) a = a
                                                                def InfTopHom.comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Min α] [Top α] [Min β] [Top β] [Min γ] [Top γ] (f : InfTopHom β γ) (g : InfTopHom α β) :
                                                                InfTopHom α γ

                                                                Composition of InfTopHoms as an InfTopHom.

                                                                Equations
                                                                • f.comp g = { toInfHom := f.comp g.toInfHom, map_top' := }
                                                                Instances For
                                                                  @[simp]
                                                                  theorem InfTopHom.coe_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Min α] [Top α] [Min β] [Top β] [Min γ] [Top γ] (f : InfTopHom β γ) (g : InfTopHom α β) :
                                                                  (f.comp g) = f g
                                                                  @[simp]
                                                                  theorem InfTopHom.comp_apply {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Min α] [Top α] [Min β] [Top β] [Min γ] [Top γ] (f : InfTopHom β γ) (g : InfTopHom α β) (a : α) :
                                                                  (f.comp g) a = f (g a)
                                                                  @[simp]
                                                                  theorem InfTopHom.comp_assoc {α : Type u_3} {β : Type u_4} {γ : Type u_5} {δ : Type u_6} [Min α] [Top α] [Min β] [Top β] [Min γ] [Top γ] [Min δ] [Top δ] (f : InfTopHom γ δ) (g : InfTopHom β γ) (h : InfTopHom α β) :
                                                                  (f.comp g).comp h = f.comp (g.comp h)
                                                                  @[simp]
                                                                  theorem InfTopHom.comp_id {α : Type u_3} {β : Type u_4} [Min α] [Top α] [Min β] [Top β] (f : InfTopHom α β) :
                                                                  f.comp (InfTopHom.id α) = f
                                                                  @[simp]
                                                                  theorem InfTopHom.id_comp {α : Type u_3} {β : Type u_4} [Min α] [Top α] [Min β] [Top β] (f : InfTopHom α β) :
                                                                  (InfTopHom.id β).comp f = f
                                                                  @[simp]
                                                                  theorem InfTopHom.cancel_right {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Min α] [Top α] [Min β] [Top β] [Min γ] [Top γ] {g₁ : InfTopHom β γ} {g₂ : InfTopHom β γ} {f : InfTopHom α β} (hf : Function.Surjective f) :
                                                                  g₁.comp f = g₂.comp f g₁ = g₂
                                                                  @[simp]
                                                                  theorem InfTopHom.cancel_left {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Min α] [Top α] [Min β] [Top β] [Min γ] [Top γ] {g : InfTopHom β γ} {f₁ : InfTopHom α β} {f₂ : InfTopHom α β} (hg : Function.Injective g) :
                                                                  g.comp f₁ = g.comp f₂ f₁ = f₂
                                                                  instance InfTopHom.instMin {α : Type u_3} {β : Type u_4} [Min α] [Top α] [SemilatticeInf β] [OrderTop β] :
                                                                  Min (InfTopHom α β)
                                                                  Equations
                                                                  • InfTopHom.instMin = { min := fun (f g : InfTopHom α β) => let __src := f.toTopHom g.toTopHom; { toInfHom := f.toInfHom g.toInfHom, map_top' := } }
                                                                  instance InfTopHom.instSemilatticeInf {α : Type u_3} {β : Type u_4} [Min α] [Top α] [SemilatticeInf β] [OrderTop β] :
                                                                  Equations
                                                                  instance InfTopHom.instOrderTop {α : Type u_3} {β : Type u_4} [Min α] [Top α] [SemilatticeInf β] [OrderTop β] :
                                                                  Equations
                                                                  @[simp]
                                                                  theorem InfTopHom.coe_inf {α : Type u_3} {β : Type u_4} [Min α] [Top α] [SemilatticeInf β] [OrderTop β] (f : InfTopHom α β) (g : InfTopHom α β) :
                                                                  (f g) = (f g)
                                                                  @[simp]
                                                                  theorem InfTopHom.coe_top {α : Type u_3} {β : Type u_4} [Min α] [Top α] [SemilatticeInf β] [OrderTop β] :
                                                                  =
                                                                  @[simp]
                                                                  theorem InfTopHom.inf_apply {α : Type u_3} {β : Type u_4} [Min α] [Top α] [SemilatticeInf β] [OrderTop β] (f : InfTopHom α β) (g : InfTopHom α β) (a : α) :
                                                                  (f g) a = f a g a
                                                                  @[simp]
                                                                  theorem InfTopHom.top_apply {α : Type u_3} {β : Type u_4} [Min α] [Top α] [SemilatticeInf β] [OrderTop β] (a : α) :
                                                                  def InfTopHom.subtypeVal {β : Type u_4} [SemilatticeInf β] [OrderTop β] {P : βProp} (Ptop : P ) (Pinf : ∀ ⦃x y : β⦄, P xP yP (x y)) :
                                                                  InfTopHom { x : β // P x } β

                                                                  Subtype.val as an InfTopHom.

                                                                  Equations
                                                                  Instances For
                                                                    @[simp]
                                                                    theorem InfTopHom.subtypeVal_apply {β : Type u_4} [SemilatticeInf β] [OrderTop β] {P : βProp} (Ptop : P ) (Pinf : ∀ ⦃x y : β⦄, P xP yP (x y)) (x : { x : β // P x }) :
                                                                    (InfTopHom.subtypeVal Ptop Pinf) x = x
                                                                    @[simp]
                                                                    theorem InfTopHom.subtypeVal_coe {β : Type u_4} [SemilatticeInf β] [OrderTop β] {P : βProp} (Ptop : P ) (Pinf : ∀ ⦃x y : β⦄, P xP yP (x y)) :
                                                                    (InfTopHom.subtypeVal Ptop Pinf) = Subtype.val

                                                                    Lattice homomorphisms #

                                                                    def LatticeHom.toInfHom {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] (f : LatticeHom α β) :
                                                                    InfHom α β

                                                                    Reinterpret a LatticeHom as an InfHom.

                                                                    Equations
                                                                    • f.toInfHom = { toFun := f.toFun, map_inf' := }
                                                                    Instances For
                                                                      instance LatticeHom.instFunLike {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] :
                                                                      FunLike (LatticeHom α β) α β
                                                                      Equations
                                                                      • LatticeHom.instFunLike = { coe := fun (f : LatticeHom α β) => f.toFun, coe_injective' := }
                                                                      instance LatticeHom.instLatticeHomClass {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] :
                                                                      Equations
                                                                      • =
                                                                      theorem LatticeHom.toFun_eq_coe {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] (f : LatticeHom α β) :
                                                                      f.toFun = f
                                                                      @[simp]
                                                                      theorem LatticeHom.coe_toSupHom {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] (f : LatticeHom α β) :
                                                                      f.toSupHom = f
                                                                      @[simp]
                                                                      theorem LatticeHom.coe_toInfHom {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] (f : LatticeHom α β) :
                                                                      f.toInfHom = f
                                                                      @[simp]
                                                                      theorem LatticeHom.coe_mk {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] (f : SupHom α β) (hf : ∀ (a b : α), f.toFun (a b) = f.toFun a f.toFun b) :
                                                                      { toSupHom := f, map_inf' := hf } = f
                                                                      theorem LatticeHom.ext {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] {f : LatticeHom α β} {g : LatticeHom α β} (h : ∀ (a : α), f a = g a) :
                                                                      f = g
                                                                      def LatticeHom.copy {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] (f : LatticeHom α β) (f' : αβ) (h : f' = f) :

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

                                                                      Equations
                                                                      • f.copy f' h = { toSupHom := f.copy f' h, map_inf' := }
                                                                      Instances For
                                                                        @[simp]
                                                                        theorem LatticeHom.coe_copy {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] (f : LatticeHom α β) (f' : αβ) (h : f' = f) :
                                                                        (f.copy f' h) = f'
                                                                        theorem LatticeHom.copy_eq {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] (f : LatticeHom α β) (f' : αβ) (h : f' = f) :
                                                                        f.copy f' h = f
                                                                        def LatticeHom.id (α : Type u_3) [Lattice α] :

                                                                        id as a LatticeHom.

                                                                        Equations
                                                                        Instances For
                                                                          instance LatticeHom.instInhabited (α : Type u_3) [Lattice α] :
                                                                          Equations
                                                                          @[simp]
                                                                          theorem LatticeHom.coe_id (α : Type u_3) [Lattice α] :
                                                                          (LatticeHom.id α) = id
                                                                          @[simp]
                                                                          theorem LatticeHom.id_apply {α : Type u_3} [Lattice α] (a : α) :
                                                                          (LatticeHom.id α) a = a
                                                                          def LatticeHom.comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Lattice α] [Lattice β] [Lattice γ] (f : LatticeHom β γ) (g : LatticeHom α β) :

                                                                          Composition of LatticeHoms as a LatticeHom.

                                                                          Equations
                                                                          • f.comp g = { toSupHom := f.comp g.toSupHom, map_inf' := }
                                                                          Instances For
                                                                            @[simp]
                                                                            theorem LatticeHom.coe_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Lattice α] [Lattice β] [Lattice γ] (f : LatticeHom β γ) (g : LatticeHom α β) :
                                                                            (f.comp g) = f g
                                                                            @[simp]
                                                                            theorem LatticeHom.comp_apply {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Lattice α] [Lattice β] [Lattice γ] (f : LatticeHom β γ) (g : LatticeHom α β) (a : α) :
                                                                            (f.comp g) a = f (g a)
                                                                            @[simp]
                                                                            theorem LatticeHom.coe_comp_sup_hom' {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Lattice α] [Lattice β] [Lattice γ] (f : LatticeHom β γ) (g : LatticeHom α β) :
                                                                            { toFun := f g, map_sup' := } = { toFun := f, map_sup' := }.comp { toFun := g, map_sup' := }
                                                                            theorem LatticeHom.coe_comp_sup_hom {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Lattice α] [Lattice β] [Lattice γ] (f : LatticeHom β γ) (g : LatticeHom α β) :
                                                                            { toFun := (f.comp g), map_sup' := } = { toFun := f, map_sup' := }.comp { toFun := g, map_sup' := }
                                                                            @[simp]
                                                                            theorem LatticeHom.coe_comp_inf_hom' {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Lattice α] [Lattice β] [Lattice γ] (f : LatticeHom β γ) (g : LatticeHom α β) :
                                                                            { toFun := f g, map_inf' := } = { toFun := f, map_inf' := }.comp { toFun := g, map_inf' := }
                                                                            theorem LatticeHom.coe_comp_inf_hom {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Lattice α] [Lattice β] [Lattice γ] (f : LatticeHom β γ) (g : LatticeHom α β) :
                                                                            { toFun := (f.comp g), map_inf' := } = { toFun := f, map_inf' := }.comp { toFun := g, map_inf' := }
                                                                            @[simp]
                                                                            theorem LatticeHom.comp_assoc {α : Type u_3} {β : Type u_4} {γ : Type u_5} {δ : Type u_6} [Lattice α] [Lattice β] [Lattice γ] [Lattice δ] (f : LatticeHom γ δ) (g : LatticeHom β γ) (h : LatticeHom α β) :
                                                                            (f.comp g).comp h = f.comp (g.comp h)
                                                                            @[simp]
                                                                            theorem LatticeHom.comp_id {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] (f : LatticeHom α β) :
                                                                            f.comp (LatticeHom.id α) = f
                                                                            @[simp]
                                                                            theorem LatticeHom.id_comp {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] (f : LatticeHom α β) :
                                                                            (LatticeHom.id β).comp f = f
                                                                            @[simp]
                                                                            theorem LatticeHom.cancel_right {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Lattice α] [Lattice β] [Lattice γ] {g₁ : LatticeHom β γ} {g₂ : LatticeHom β γ} {f : LatticeHom α β} (hf : Function.Surjective f) :
                                                                            g₁.comp f = g₂.comp f g₁ = g₂
                                                                            @[simp]
                                                                            theorem LatticeHom.cancel_left {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Lattice α] [Lattice β] [Lattice γ] {g : LatticeHom β γ} {f₁ : LatticeHom α β} {f₂ : LatticeHom α β} (hg : Function.Injective g) :
                                                                            g.comp f₁ = g.comp f₂ f₁ = f₂
                                                                            def LatticeHom.subtypeVal {β : Type u_4} [Lattice β] {P : βProp} (Psup : ∀ ⦃x y : β⦄, P xP yP (x y)) (Pinf : ∀ ⦃x y : β⦄, P xP yP (x y)) :
                                                                            LatticeHom { x : β // P x } β

                                                                            Subtype.val as a LatticeHom.

                                                                            Equations
                                                                            Instances For
                                                                              @[simp]
                                                                              theorem LatticeHom.subtypeVal_apply {β : Type u_4} [Lattice β] {P : βProp} (Psup : ∀ ⦃x y : β⦄, P xP yP (x y)) (Pinf : ∀ ⦃x y : β⦄, P xP yP (x y)) (x : { x : β // P x }) :
                                                                              (LatticeHom.subtypeVal Psup Pinf) x = x
                                                                              @[simp]
                                                                              theorem LatticeHom.subtypeVal_coe {β : Type u_4} [Lattice β] {P : βProp} (Psup : ∀ ⦃x y : β⦄, P xP yP (x y)) (Pinf : ∀ ⦃x y : β⦄, P xP yP (x y)) :
                                                                              (LatticeHom.subtypeVal Psup Pinf) = Subtype.val
                                                                              @[instance 100]
                                                                              instance OrderHomClass.toLatticeHomClass {F : Type u_1} (α : Type u_3) (β : Type u_4) [FunLike F α β] [LinearOrder α] [Lattice β] [OrderHomClass F α β] :

                                                                              An order homomorphism from a linear order is a lattice homomorphism.

                                                                              Equations
                                                                              • =
                                                                              def OrderHomClass.toLatticeHom {F : Type u_1} (α : Type u_3) (β : Type u_4) [FunLike F α β] [LinearOrder α] [Lattice β] [OrderHomClass F α β] (f : F) :

                                                                              Reinterpret an order homomorphism to a linear order as a LatticeHom.

                                                                              Equations
                                                                              Instances For
                                                                                @[simp]
                                                                                theorem OrderHomClass.coe_to_lattice_hom {F : Type u_1} (α : Type u_3) (β : Type u_4) [FunLike F α β] [LinearOrder α] [Lattice β] [OrderHomClass F α β] (f : F) :
                                                                                (OrderHomClass.toLatticeHom α β f) = f
                                                                                @[simp]
                                                                                theorem OrderHomClass.to_lattice_hom_apply {F : Type u_1} (α : Type u_3) (β : Type u_4) [FunLike F α β] [LinearOrder α] [Lattice β] [OrderHomClass F α β] (f : F) (a : α) :

                                                                                Bounded lattice homomorphisms #

                                                                                def BoundedLatticeHom.toSupBotHom {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] [BoundedOrder α] [BoundedOrder β] (f : BoundedLatticeHom α β) :
                                                                                SupBotHom α β

                                                                                Reinterpret a BoundedLatticeHom as a SupBotHom.

                                                                                Equations
                                                                                • f.toSupBotHom = { toSupHom := f.toSupHom, map_bot' := }
                                                                                Instances For
                                                                                  def BoundedLatticeHom.toInfTopHom {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] [BoundedOrder α] [BoundedOrder β] (f : BoundedLatticeHom α β) :
                                                                                  InfTopHom α β

                                                                                  Reinterpret a BoundedLatticeHom as an InfTopHom.

                                                                                  Equations
                                                                                  • f.toInfTopHom = { toFun := f.toFun, map_inf' := , map_top' := }
                                                                                  Instances For

                                                                                    Reinterpret a BoundedLatticeHom as a BoundedOrderHom.

                                                                                    Equations
                                                                                    • f.toBoundedOrderHom = { toFun := f.toFun, monotone' := , map_top' := , map_bot' := }
                                                                                    Instances For
                                                                                      instance BoundedLatticeHom.instFunLike {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] [BoundedOrder α] [BoundedOrder β] :
                                                                                      Equations
                                                                                      • BoundedLatticeHom.instFunLike = { coe := fun (f : BoundedLatticeHom α β) => f.toFun, coe_injective' := }
                                                                                      Equations
                                                                                      • =
                                                                                      @[simp]
                                                                                      theorem BoundedLatticeHom.toFun_eq_coe {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] [BoundedOrder α] [BoundedOrder β] (f : BoundedLatticeHom α β) :
                                                                                      f.toFun = f
                                                                                      @[simp]
                                                                                      theorem BoundedLatticeHom.coe_toLatticeHom {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] [BoundedOrder α] [BoundedOrder β] (f : BoundedLatticeHom α β) :
                                                                                      f.toLatticeHom = f
                                                                                      @[simp]
                                                                                      theorem BoundedLatticeHom.coe_toSupBotHom {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] [BoundedOrder α] [BoundedOrder β] (f : BoundedLatticeHom α β) :
                                                                                      f.toSupBotHom = f
                                                                                      @[simp]
                                                                                      theorem BoundedLatticeHom.coe_toInfTopHom {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] [BoundedOrder α] [BoundedOrder β] (f : BoundedLatticeHom α β) :
                                                                                      f.toInfTopHom = f
                                                                                      @[simp]
                                                                                      theorem BoundedLatticeHom.coe_toBoundedOrderHom {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] [BoundedOrder α] [BoundedOrder β] (f : BoundedLatticeHom α β) :
                                                                                      f.toBoundedOrderHom = f
                                                                                      @[simp]
                                                                                      theorem BoundedLatticeHom.coe_mk {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] [BoundedOrder α] [BoundedOrder β] (f : LatticeHom α β) (hf : f.toFun = ) (hf' : f.toFun = ) :
                                                                                      { toLatticeHom := f, map_top' := hf, map_bot' := hf' } = f
                                                                                      theorem BoundedLatticeHom.ext {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] [BoundedOrder α] [BoundedOrder β] {f : BoundedLatticeHom α β} {g : BoundedLatticeHom α β} (h : ∀ (a : α), f a = g a) :
                                                                                      f = g
                                                                                      def BoundedLatticeHom.copy {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] [BoundedOrder α] [BoundedOrder β] (f : BoundedLatticeHom α β) (f' : αβ) (h : f' = f) :

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

                                                                                      Equations
                                                                                      • f.copy f' h = { toLatticeHom := f.copy f' h, map_top' := , map_bot' := }
                                                                                      Instances For
                                                                                        @[simp]
                                                                                        theorem BoundedLatticeHom.coe_copy {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] [BoundedOrder α] [BoundedOrder β] (f : BoundedLatticeHom α β) (f' : αβ) (h : f' = f) :
                                                                                        (f.copy f' h) = f'
                                                                                        theorem BoundedLatticeHom.copy_eq {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] [BoundedOrder α] [BoundedOrder β] (f : BoundedLatticeHom α β) (f' : αβ) (h : f' = f) :
                                                                                        f.copy f' h = f

                                                                                        id as a BoundedLatticeHom.

                                                                                        Equations
                                                                                        Instances For
                                                                                          @[simp]
                                                                                          theorem BoundedLatticeHom.coe_id (α : Type u_3) [Lattice α] [BoundedOrder α] :
                                                                                          @[simp]
                                                                                          theorem BoundedLatticeHom.id_apply {α : Type u_3} [Lattice α] [BoundedOrder α] (a : α) :
                                                                                          def BoundedLatticeHom.comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Lattice α] [Lattice β] [Lattice γ] [BoundedOrder α] [BoundedOrder β] [BoundedOrder γ] (f : BoundedLatticeHom β γ) (g : BoundedLatticeHom α β) :

                                                                                          Composition of BoundedLatticeHoms as a BoundedLatticeHom.

                                                                                          Equations
                                                                                          • f.comp g = { toLatticeHom := f.comp g.toLatticeHom, map_top' := , map_bot' := }
                                                                                          Instances For
                                                                                            @[simp]
                                                                                            theorem BoundedLatticeHom.coe_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Lattice α] [Lattice β] [Lattice γ] [BoundedOrder α] [BoundedOrder β] [BoundedOrder γ] (f : BoundedLatticeHom β γ) (g : BoundedLatticeHom α β) :
                                                                                            (f.comp g) = f g
                                                                                            @[simp]
                                                                                            theorem BoundedLatticeHom.comp_apply {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Lattice α] [Lattice β] [Lattice γ] [BoundedOrder α] [BoundedOrder β] [BoundedOrder γ] (f : BoundedLatticeHom β γ) (g : BoundedLatticeHom α β) (a : α) :
                                                                                            (f.comp g) a = f (g a)
                                                                                            @[simp]
                                                                                            theorem BoundedLatticeHom.coe_comp_lattice_hom' {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Lattice α] [Lattice β] [Lattice γ] [BoundedOrder α] [BoundedOrder β] [BoundedOrder γ] (f : BoundedLatticeHom β γ) (g : BoundedLatticeHom α β) :
                                                                                            { toSupHom := { toFun := f, map_sup' := }.comp { toFun := g, map_sup' := }, map_inf' := } = { toFun := f, map_sup' := , map_inf' := }.comp { toFun := g, map_sup' := , map_inf' := }
                                                                                            theorem BoundedLatticeHom.coe_comp_lattice_hom {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Lattice α] [Lattice β] [Lattice γ] [BoundedOrder α] [BoundedOrder β] [BoundedOrder γ] (f : BoundedLatticeHom β γ) (g : BoundedLatticeHom α β) :
                                                                                            { toFun := (f.comp g), map_sup' := , map_inf' := } = { toFun := f, map_sup' := , map_inf' := }.comp { toFun := g, map_sup' := , map_inf' := }
                                                                                            @[simp]
                                                                                            theorem BoundedLatticeHom.coe_comp_sup_hom' {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Lattice α] [Lattice β] [Lattice γ] [BoundedOrder α] [BoundedOrder β] [BoundedOrder γ] (f : BoundedLatticeHom β γ) (g : BoundedLatticeHom α β) :
                                                                                            { toFun := f g, map_sup' := } = { toFun := f, map_sup' := }.comp { toFun := g, map_sup' := }
                                                                                            theorem BoundedLatticeHom.coe_comp_sup_hom {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Lattice α] [Lattice β] [Lattice γ] [BoundedOrder α] [BoundedOrder β] [BoundedOrder γ] (f : BoundedLatticeHom β γ) (g : BoundedLatticeHom α β) :
                                                                                            { toFun := (f.comp g), map_sup' := } = { toFun := f, map_sup' := }.comp { toFun := g, map_sup' := }
                                                                                            @[simp]
                                                                                            theorem BoundedLatticeHom.coe_comp_inf_hom' {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Lattice α] [Lattice β] [Lattice γ] [BoundedOrder α] [BoundedOrder β] [BoundedOrder γ] (f : BoundedLatticeHom β γ) (g : BoundedLatticeHom α β) :
                                                                                            { toFun := f g, map_inf' := } = { toFun := f, map_inf' := }.comp { toFun := g, map_inf' := }
                                                                                            theorem BoundedLatticeHom.coe_comp_inf_hom {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Lattice α] [Lattice β] [Lattice γ] [BoundedOrder α] [BoundedOrder β] [BoundedOrder γ] (f : BoundedLatticeHom β γ) (g : BoundedLatticeHom α β) :
                                                                                            { toFun := (f.comp g), map_inf' := } = { toFun := f, map_inf' := }.comp { toFun := g, map_inf' := }
                                                                                            @[simp]
                                                                                            theorem BoundedLatticeHom.comp_assoc {α : Type u_3} {β : Type u_4} {γ : Type u_5} {δ : Type u_6} [Lattice α] [Lattice β] [Lattice γ] [Lattice δ] [BoundedOrder α] [BoundedOrder β] [BoundedOrder γ] [BoundedOrder δ] (f : BoundedLatticeHom γ δ) (g : BoundedLatticeHom β γ) (h : BoundedLatticeHom α β) :
                                                                                            (f.comp g).comp h = f.comp (g.comp h)
                                                                                            @[simp]
                                                                                            theorem BoundedLatticeHom.comp_id {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] [BoundedOrder α] [BoundedOrder β] (f : BoundedLatticeHom α β) :
                                                                                            f.comp (BoundedLatticeHom.id α) = f
                                                                                            @[simp]
                                                                                            theorem BoundedLatticeHom.id_comp {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] [BoundedOrder α] [BoundedOrder β] (f : BoundedLatticeHom α β) :
                                                                                            (BoundedLatticeHom.id β).comp f = f
                                                                                            @[simp]
                                                                                            theorem BoundedLatticeHom.cancel_right {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Lattice α] [Lattice β] [Lattice γ] [BoundedOrder α] [BoundedOrder β] [BoundedOrder γ] {g₁ : BoundedLatticeHom β γ} {g₂ : BoundedLatticeHom β γ} {f : BoundedLatticeHom α β} (hf : Function.Surjective f) :
                                                                                            g₁.comp f = g₂.comp f g₁ = g₂
                                                                                            @[simp]
                                                                                            theorem BoundedLatticeHom.cancel_left {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Lattice α] [Lattice β] [Lattice γ] [BoundedOrder α] [BoundedOrder β] [BoundedOrder γ] {g : BoundedLatticeHom β γ} {f₁ : BoundedLatticeHom α β} {f₂ : BoundedLatticeHom α β} (hg : Function.Injective g) :
                                                                                            g.comp f₁ = g.comp f₂ f₁ = f₂
                                                                                            def BoundedLatticeHom.subtypeVal {β : Type u_4} [Lattice β] [BoundedOrder β] {P : βProp} (Pbot : P ) (Ptop : P ) (Psup : ∀ ⦃x y : β⦄, P xP yP (x y)) (Pinf : ∀ ⦃x y : β⦄, P xP yP (x y)) :
                                                                                            BoundedLatticeHom { x : β // P x } β

                                                                                            Subtype.val as a BoundedLatticeHom.

                                                                                            Equations
                                                                                            Instances For
                                                                                              @[simp]
                                                                                              theorem BoundedLatticeHom.subtypeVal_apply {β : Type u_4} [Lattice β] [BoundedOrder β] {P : βProp} (Pbot : P ) (Ptop : P ) (Psup : ∀ ⦃x y : β⦄, P xP yP (x y)) (Pinf : ∀ ⦃x y : β⦄, P xP yP (x y)) (x : { x : β // P x }) :
                                                                                              (BoundedLatticeHom.subtypeVal Pbot Ptop Psup Pinf) x = x
                                                                                              @[simp]
                                                                                              theorem BoundedLatticeHom.subtypeVal_coe {β : Type u_4} [Lattice β] [BoundedOrder β] {P : βProp} (Pbot : P ) (Ptop : P ) (Psup : ∀ ⦃x y : β⦄, P xP yP (x y)) (Pinf : ∀ ⦃x y : β⦄, P xP yP (x y)) :
                                                                                              (BoundedLatticeHom.subtypeVal Pbot Ptop Psup Pinf) = Subtype.val

                                                                                              Dual homs #

                                                                                              def SupHom.dual {α : Type u_3} {β : Type u_4} [Max α] [Max β] :

                                                                                              Reinterpret a supremum homomorphism as an infimum homomorphism between the dual lattices.

                                                                                              Equations
                                                                                              • SupHom.dual = { toFun := fun (f : SupHom α β) => { toFun := f, map_inf' := }, invFun := fun (f : InfHom αᵒᵈ βᵒᵈ) => { toFun := f, map_sup' := }, left_inv := , right_inv := }
                                                                                              Instances For
                                                                                                @[simp]
                                                                                                theorem SupHom.dual_apply_toFun {α : Type u_3} {β : Type u_4} [Max α] [Max β] (f : SupHom α β) (a : α) :
                                                                                                (SupHom.dual f) a = f a
                                                                                                @[simp]
                                                                                                theorem SupHom.dual_symm_apply_toFun {α : Type u_3} {β : Type u_4} [Max α] [Max β] (f : InfHom αᵒᵈ βᵒᵈ) (a : αᵒᵈ) :
                                                                                                (SupHom.dual.symm f) a = f a
                                                                                                @[simp]
                                                                                                theorem SupHom.dual_id {α : Type u_3} [Max α] :
                                                                                                SupHom.dual (SupHom.id α) = InfHom.id αᵒᵈ
                                                                                                @[simp]
                                                                                                theorem SupHom.dual_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Max α] [Max β] [Max γ] (g : SupHom β γ) (f : SupHom α β) :
                                                                                                SupHom.dual (g.comp f) = (SupHom.dual g).comp (SupHom.dual f)
                                                                                                @[simp]
                                                                                                theorem SupHom.symm_dual_id {α : Type u_3} [Max α] :
                                                                                                SupHom.dual.symm (InfHom.id αᵒᵈ) = SupHom.id α
                                                                                                @[simp]
                                                                                                theorem SupHom.symm_dual_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Max α] [Max β] [Max γ] (g : InfHom βᵒᵈ γᵒᵈ) (f : InfHom αᵒᵈ βᵒᵈ) :
                                                                                                SupHom.dual.symm (g.comp f) = (SupHom.dual.symm g).comp (SupHom.dual.symm f)
                                                                                                def InfHom.dual {α : Type u_3} {β : Type u_4} [Min α] [Min β] :

                                                                                                Reinterpret an infimum homomorphism as a supremum homomorphism between the dual lattices.

                                                                                                Equations
                                                                                                • InfHom.dual = { toFun := fun (f : InfHom α β) => { toFun := f, map_sup' := }, invFun := fun (f : SupHom αᵒᵈ βᵒᵈ) => { toFun := f, map_inf' := }, left_inv := , right_inv := }
                                                                                                Instances For
                                                                                                  @[simp]
                                                                                                  theorem InfHom.dual_symm_apply_toFun {α : Type u_3} {β : Type u_4} [Min α] [Min β] (f : SupHom αᵒᵈ βᵒᵈ) (a : αᵒᵈ) :
                                                                                                  (InfHom.dual.symm f) a = f a
                                                                                                  @[simp]
                                                                                                  theorem InfHom.dual_apply_toFun {α : Type u_3} {β : Type u_4} [Min α] [Min β] (f : InfHom α β) (a : α) :
                                                                                                  (InfHom.dual f) a = f a
                                                                                                  @[simp]
                                                                                                  theorem InfHom.dual_id {α : Type u_3} [Min α] :
                                                                                                  InfHom.dual (InfHom.id α) = SupHom.id αᵒᵈ
                                                                                                  @[simp]
                                                                                                  theorem InfHom.dual_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Min α] [Min β] [Min γ] (g : InfHom β γ) (f : InfHom α β) :
                                                                                                  InfHom.dual (g.comp f) = (InfHom.dual g).comp (InfHom.dual f)
                                                                                                  @[simp]
                                                                                                  theorem InfHom.symm_dual_id {α : Type u_3} [Min α] :
                                                                                                  InfHom.dual.symm (SupHom.id αᵒᵈ) = InfHom.id α
                                                                                                  @[simp]
                                                                                                  theorem InfHom.symm_dual_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Min α] [Min β] [Min γ] (g : SupHom βᵒᵈ γᵒᵈ) (f : SupHom αᵒᵈ βᵒᵈ) :
                                                                                                  InfHom.dual.symm (g.comp f) = (InfHom.dual.symm g).comp (InfHom.dual.symm f)
                                                                                                  def SupBotHom.dual {α : Type u_3} {β : Type u_4} [Max α] [Bot α] [Max β] [Bot β] :

                                                                                                  Reinterpret a finitary supremum homomorphism as a finitary infimum homomorphism between the dual lattices.

                                                                                                  Equations
                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                  Instances For
                                                                                                    @[simp]
                                                                                                    theorem SupBotHom.dual_id {α : Type u_3} [Max α] [Bot α] :
                                                                                                    SupBotHom.dual (SupBotHom.id α) = InfTopHom.id αᵒᵈ
                                                                                                    @[simp]
                                                                                                    theorem SupBotHom.dual_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Max α] [Bot α] [Max β] [Bot β] [Max γ] [Bot γ] (g : SupBotHom β γ) (f : SupBotHom α β) :
                                                                                                    SupBotHom.dual (g.comp f) = (SupBotHom.dual g).comp (SupBotHom.dual f)
                                                                                                    @[simp]
                                                                                                    theorem SupBotHom.symm_dual_id {α : Type u_3} [Max α] [Bot α] :
                                                                                                    SupBotHom.dual.symm (InfTopHom.id αᵒᵈ) = SupBotHom.id α
                                                                                                    @[simp]
                                                                                                    theorem SupBotHom.symm_dual_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Max α] [Bot α] [Max β] [Bot β] [Max γ] [Bot γ] (g : InfTopHom βᵒᵈ γᵒᵈ) (f : InfTopHom αᵒᵈ βᵒᵈ) :
                                                                                                    SupBotHom.dual.symm (g.comp f) = (SupBotHom.dual.symm g).comp (SupBotHom.dual.symm f)
                                                                                                    def InfTopHom.dual {α : Type u_3} {β : Type u_4} [Min α] [Top α] [Min β] [Top β] :

                                                                                                    Reinterpret a finitary infimum homomorphism as a finitary supremum homomorphism between the dual lattices.

                                                                                                    Equations
                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                    Instances For
                                                                                                      @[simp]
                                                                                                      theorem InfTopHom.dual_symm_apply_toInfHom {α : Type u_3} {β : Type u_4} [Min α] [Top α] [Min β] [Top β] (f : SupBotHom αᵒᵈ βᵒᵈ) :
                                                                                                      (InfTopHom.dual.symm f).toInfHom = InfHom.dual.symm f.toSupHom
                                                                                                      @[simp]
                                                                                                      theorem InfTopHom.dual_apply_toSupHom {α : Type u_3} {β : Type u_4} [Min α] [Top α] [Min β] [Top β] (f : InfTopHom α β) :
                                                                                                      (InfTopHom.dual f).toSupHom = InfHom.dual f.toInfHom
                                                                                                      @[simp]
                                                                                                      theorem InfTopHom.dual_id {α : Type u_3} [Min α] [Top α] :
                                                                                                      InfTopHom.dual (InfTopHom.id α) = SupBotHom.id αᵒᵈ
                                                                                                      @[simp]
                                                                                                      theorem InfTopHom.dual_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Min α] [Top α] [Min β] [Top β] [Min γ] [Top γ] (g : InfTopHom β γ) (f : InfTopHom α β) :
                                                                                                      InfTopHom.dual (g.comp f) = (InfTopHom.dual g).comp (InfTopHom.dual f)
                                                                                                      @[simp]
                                                                                                      theorem InfTopHom.symm_dual_id {α : Type u_3} [Min α] [Top α] :
                                                                                                      InfTopHom.dual.symm (SupBotHom.id αᵒᵈ) = InfTopHom.id α
                                                                                                      @[simp]
                                                                                                      theorem InfTopHom.symm_dual_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Min α] [Top α] [Min β] [Top β] [Min γ] [Top γ] (g : SupBotHom βᵒᵈ γᵒᵈ) (f : SupBotHom αᵒᵈ βᵒᵈ) :
                                                                                                      InfTopHom.dual.symm (g.comp f) = (InfTopHom.dual.symm g).comp (InfTopHom.dual.symm f)
                                                                                                      def LatticeHom.dual {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] :

                                                                                                      Reinterpret a lattice homomorphism as a lattice homomorphism between the dual lattices.

                                                                                                      Equations
                                                                                                      • One or more equations did not get rendered due to their size.
                                                                                                      Instances For
                                                                                                        @[simp]
                                                                                                        theorem LatticeHom.dual_symm_apply_toSupHom {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] (f : LatticeHom αᵒᵈ βᵒᵈ) :
                                                                                                        (LatticeHom.dual.symm f).toSupHom = SupHom.dual.symm f.toInfHom
                                                                                                        @[simp]
                                                                                                        theorem LatticeHom.dual_apply_toSupHom {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] (f : LatticeHom α β) :
                                                                                                        (LatticeHom.dual f).toSupHom = InfHom.dual f.toInfHom
                                                                                                        @[simp]
                                                                                                        theorem LatticeHom.dual_id {α : Type u_3} [Lattice α] :
                                                                                                        LatticeHom.dual (LatticeHom.id α) = LatticeHom.id αᵒᵈ
                                                                                                        @[simp]
                                                                                                        theorem LatticeHom.dual_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Lattice α] [Lattice β] [Lattice γ] (g : LatticeHom β γ) (f : LatticeHom α β) :
                                                                                                        LatticeHom.dual (g.comp f) = (LatticeHom.dual g).comp (LatticeHom.dual f)
                                                                                                        @[simp]
                                                                                                        theorem LatticeHom.symm_dual_id {α : Type u_3} [Lattice α] :
                                                                                                        LatticeHom.dual.symm (LatticeHom.id αᵒᵈ) = LatticeHom.id α
                                                                                                        @[simp]
                                                                                                        theorem LatticeHom.symm_dual_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Lattice α] [Lattice β] [Lattice γ] (g : LatticeHom βᵒᵈ γᵒᵈ) (f : LatticeHom αᵒᵈ βᵒᵈ) :
                                                                                                        LatticeHom.dual.symm (g.comp f) = (LatticeHom.dual.symm g).comp (LatticeHom.dual.symm f)

                                                                                                        Reinterpret a bounded lattice homomorphism as a bounded lattice homomorphism between the dual bounded lattices.

                                                                                                        Equations
                                                                                                        • One or more equations did not get rendered due to their size.
                                                                                                        Instances For
                                                                                                          @[simp]
                                                                                                          theorem BoundedLatticeHom.dual_symm_apply_toLatticeHom {α : Type u_3} {β : Type u_4} [Lattice α] [BoundedOrder α] [Lattice β] [BoundedOrder β] (f : BoundedLatticeHom αᵒᵈ βᵒᵈ) :
                                                                                                          (BoundedLatticeHom.dual.symm f).toLatticeHom = LatticeHom.dual.symm f.toLatticeHom
                                                                                                          @[simp]
                                                                                                          theorem BoundedLatticeHom.dual_apply_toLatticeHom {α : Type u_3} {β : Type u_4} [Lattice α] [BoundedOrder α] [Lattice β] [BoundedOrder β] (f : BoundedLatticeHom α β) :
                                                                                                          (BoundedLatticeHom.dual f).toLatticeHom = LatticeHom.dual f.toLatticeHom
                                                                                                          @[simp]
                                                                                                          theorem BoundedLatticeHom.dual_id {α : Type u_3} [Lattice α] [BoundedOrder α] :
                                                                                                          BoundedLatticeHom.dual (BoundedLatticeHom.id α) = BoundedLatticeHom.id αᵒᵈ
                                                                                                          @[simp]
                                                                                                          theorem BoundedLatticeHom.dual_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Lattice α] [BoundedOrder α] [Lattice β] [BoundedOrder β] [Lattice γ] [BoundedOrder γ] (g : BoundedLatticeHom β γ) (f : BoundedLatticeHom α β) :
                                                                                                          BoundedLatticeHom.dual (g.comp f) = (BoundedLatticeHom.dual g).comp (BoundedLatticeHom.dual f)
                                                                                                          @[simp]
                                                                                                          theorem BoundedLatticeHom.symm_dual_id {α : Type u_3} [Lattice α] [BoundedOrder α] :
                                                                                                          BoundedLatticeHom.dual.symm (BoundedLatticeHom.id αᵒᵈ) = BoundedLatticeHom.id α
                                                                                                          @[simp]
                                                                                                          theorem BoundedLatticeHom.symm_dual_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Lattice α] [BoundedOrder α] [Lattice β] [BoundedOrder β] [Lattice γ] [BoundedOrder γ] (g : BoundedLatticeHom βᵒᵈ γᵒᵈ) (f : BoundedLatticeHom αᵒᵈ βᵒᵈ) :
                                                                                                          BoundedLatticeHom.dual.symm (g.comp f) = (BoundedLatticeHom.dual.symm g).comp (BoundedLatticeHom.dual.symm f)

                                                                                                          Prod #

                                                                                                          def LatticeHom.fst {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] :
                                                                                                          LatticeHom (α × β) α

                                                                                                          Natural projection homomorphism from α × β to α.

                                                                                                          Equations
                                                                                                          • LatticeHom.fst = { toFun := Prod.fst, map_sup' := , map_inf' := }
                                                                                                          Instances For
                                                                                                            def LatticeHom.snd {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] :
                                                                                                            LatticeHom (α × β) β

                                                                                                            Natural projection homomorphism from α × β to β.

                                                                                                            Equations
                                                                                                            • LatticeHom.snd = { toFun := Prod.snd, map_sup' := , map_inf' := }
                                                                                                            Instances For
                                                                                                              @[simp]
                                                                                                              theorem LatticeHom.coe_fst {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] :
                                                                                                              LatticeHom.fst = Prod.fst
                                                                                                              @[simp]
                                                                                                              theorem LatticeHom.coe_snd {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] :
                                                                                                              LatticeHom.snd = Prod.snd
                                                                                                              theorem LatticeHom.fst_apply {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] (x : α × β) :
                                                                                                              LatticeHom.fst x = x.1
                                                                                                              theorem LatticeHom.snd_apply {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] (x : α × β) :
                                                                                                              LatticeHom.snd x = x.2

                                                                                                              Pi #

                                                                                                              def Pi.evalLatticeHom {ι : Type u_7} {α : ιType u_8} [(i : ι) → Lattice (α i)] (i : ι) :
                                                                                                              LatticeHom ((i : ι) → α i) (α i)

                                                                                                              Evaluation as a lattice homomorphism.

                                                                                                              Equations
                                                                                                              Instances For
                                                                                                                @[simp]
                                                                                                                theorem Pi.coe_evalLatticeHom {ι : Type u_7} {α : ιType u_8} [(i : ι) → Lattice (α i)] (i : ι) :
                                                                                                                theorem Pi.evalLatticeHom_apply {ι : Type u_7} {α : ιType u_8} [(i : ι) → Lattice (α i)] (i : ι) (f : (i : ι) → α i) :

                                                                                                                WithTop, WithBot #

                                                                                                                def SupHom.withTop {α : Type u_3} {β : Type u_4} [SemilatticeSup α] [SemilatticeSup β] (f : SupHom α β) :

                                                                                                                Adjoins a to the domain and codomain of a SupHom.

                                                                                                                Equations
                                                                                                                Instances For
                                                                                                                  @[simp]
                                                                                                                  theorem SupHom.withTop_toFun {α : Type u_3} {β : Type u_4} [SemilatticeSup α] [SemilatticeSup β] (f : SupHom α β) :
                                                                                                                  ∀ (a : WithTop α), f.withTop a = WithTop.map (⇑f) a
                                                                                                                  @[simp]
                                                                                                                  theorem SupHom.withTop_id {α : Type u_3} [SemilatticeSup α] :
                                                                                                                  (SupHom.id α).withTop = SupHom.id (WithTop α)
                                                                                                                  @[simp]
                                                                                                                  theorem SupHom.withTop_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [SemilatticeSup α] [SemilatticeSup β] [SemilatticeSup γ] (f : SupHom β γ) (g : SupHom α β) :
                                                                                                                  (f.comp g).withTop = f.withTop.comp g.withTop
                                                                                                                  def SupHom.withBot {α : Type u_3} {β : Type u_4} [SemilatticeSup α] [SemilatticeSup β] (f : SupHom α β) :

                                                                                                                  Adjoins a to the domain and codomain of a SupHom.

                                                                                                                  Equations
                                                                                                                  • f.withBot = { toFun := Option.map f, map_sup' := , map_bot' := }
                                                                                                                  Instances For
                                                                                                                    @[simp]
                                                                                                                    theorem SupHom.withBot_toSupHom_toFun {α : Type u_3} {β : Type u_4} [SemilatticeSup α] [SemilatticeSup β] (f : SupHom α β) :
                                                                                                                    ∀ (a : Option α), f.withBot.toSupHom a = Option.map (⇑f) a
                                                                                                                    @[simp]
                                                                                                                    theorem SupHom.withBot_id {α : Type u_3} [SemilatticeSup α] :
                                                                                                                    (SupHom.id α).withBot = SupBotHom.id (WithBot α)
                                                                                                                    @[simp]
                                                                                                                    theorem SupHom.withBot_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [SemilatticeSup α] [SemilatticeSup β] [SemilatticeSup γ] (f : SupHom β γ) (g : SupHom α β) :
                                                                                                                    (f.comp g).withBot = f.withBot.comp g.withBot
                                                                                                                    def SupHom.withTop' {α : Type u_3} {β : Type u_4} [SemilatticeSup α] [SemilatticeSup β] [OrderTop β] (f : SupHom α β) :
                                                                                                                    SupHom (WithTop α) β

                                                                                                                    Adjoins a to the codomain of a SupHom.

                                                                                                                    Equations
                                                                                                                    Instances For
                                                                                                                      @[simp]
                                                                                                                      theorem SupHom.withTop'_toFun {α : Type u_3} {β : Type u_4} [SemilatticeSup α] [SemilatticeSup β] [OrderTop β] (f : SupHom α β) (a : WithTop α) :
                                                                                                                      f.withTop' a = Option.elim a f
                                                                                                                      def SupHom.withBot' {α : Type u_3} {β : Type u_4} [SemilatticeSup α] [SemilatticeSup β] [OrderBot β] (f : SupHom α β) :

                                                                                                                      Adjoins a to the domain of a SupHom.

                                                                                                                      Equations
                                                                                                                      Instances For
                                                                                                                        @[simp]
                                                                                                                        theorem SupHom.withBot'_toSupHom_toFun {α : Type u_3} {β : Type u_4} [SemilatticeSup α] [SemilatticeSup β] [OrderBot β] (f : SupHom α β) (a : WithBot α) :
                                                                                                                        f.withBot'.toSupHom a = Option.elim a f
                                                                                                                        def InfHom.withTop {α : Type u_3} {β : Type u_4} [SemilatticeInf α] [SemilatticeInf β] (f : InfHom α β) :

                                                                                                                        Adjoins a to the domain and codomain of an InfHom.

                                                                                                                        Equations
                                                                                                                        • f.withTop = { toFun := Option.map f, map_inf' := , map_top' := }
                                                                                                                        Instances For
                                                                                                                          @[simp]
                                                                                                                          theorem InfHom.withTop_toInfHom_toFun {α : Type u_3} {β : Type u_4} [SemilatticeInf α] [SemilatticeInf β] (f : InfHom α β) :
                                                                                                                          ∀ (a : Option α), f.withTop.toInfHom a = Option.map (⇑f) a
                                                                                                                          @[simp]
                                                                                                                          theorem InfHom.withTop_id {α : Type u_3} [SemilatticeInf α] :
                                                                                                                          (InfHom.id α).withTop = InfTopHom.id (WithTop α)
                                                                                                                          @[simp]
                                                                                                                          theorem InfHom.withTop_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [SemilatticeInf α] [SemilatticeInf β] [SemilatticeInf γ] (f : InfHom β γ) (g : InfHom α β) :
                                                                                                                          (f.comp g).withTop = f.withTop.comp g.withTop
                                                                                                                          def InfHom.withBot {α : Type u_3} {β : Type u_4} [SemilatticeInf α] [SemilatticeInf β] (f : InfHom α β) :

                                                                                                                          Adjoins a to the domain and codomain of an InfHom.

                                                                                                                          Equations
                                                                                                                          • f.withBot = { toFun := Option.map f, map_inf' := }
                                                                                                                          Instances For
                                                                                                                            @[simp]
                                                                                                                            theorem InfHom.withBot_toFun {α : Type u_3} {β : Type u_4} [SemilatticeInf α] [SemilatticeInf β] (f : InfHom α β) :
                                                                                                                            ∀ (a : Option α), f.withBot a = Option.map (⇑f) a
                                                                                                                            @[simp]
                                                                                                                            theorem InfHom.withBot_id {α : Type u_3} [SemilatticeInf α] :
                                                                                                                            (InfHom.id α).withBot = InfHom.id (WithBot α)
                                                                                                                            @[simp]
                                                                                                                            theorem InfHom.withBot_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [SemilatticeInf α] [SemilatticeInf β] [SemilatticeInf γ] (f : InfHom β γ) (g : InfHom α β) :
                                                                                                                            (f.comp g).withBot = f.withBot.comp g.withBot
                                                                                                                            def InfHom.withTop' {α : Type u_3} {β : Type u_4} [SemilatticeInf α] [SemilatticeInf β] [OrderTop β] (f : InfHom α β) :

                                                                                                                            Adjoins a to the codomain of an InfHom.

                                                                                                                            Equations
                                                                                                                            Instances For
                                                                                                                              @[simp]
                                                                                                                              theorem InfHom.withTop'_toInfHom_toFun {α : Type u_3} {β : Type u_4} [SemilatticeInf α] [SemilatticeInf β] [OrderTop β] (f : InfHom α β) (a : WithTop α) :
                                                                                                                              f.withTop'.toInfHom a = Option.elim a f
                                                                                                                              def InfHom.withBot' {α : Type u_3} {β : Type u_4} [SemilatticeInf α] [SemilatticeInf β] [OrderBot β] (f : InfHom α β) :
                                                                                                                              InfHom (WithBot α) β

                                                                                                                              Adjoins a to the codomain of an InfHom.

                                                                                                                              Equations
                                                                                                                              Instances For
                                                                                                                                @[simp]
                                                                                                                                theorem InfHom.withBot'_toFun {α : Type u_3} {β : Type u_4} [SemilatticeInf α] [SemilatticeInf β] [OrderBot β] (f : InfHom α β) (a : WithBot α) :
                                                                                                                                f.withBot' a = Option.elim a f
                                                                                                                                def LatticeHom.withTop {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] (f : LatticeHom α β) :

                                                                                                                                Adjoins a to the domain and codomain of a LatticeHom.

                                                                                                                                Equations
                                                                                                                                • f.withTop = { toSupHom := f.withTop, map_inf' := }
                                                                                                                                Instances For
                                                                                                                                  @[simp]
                                                                                                                                  theorem LatticeHom.withTop_toSupHom {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] (f : LatticeHom α β) :
                                                                                                                                  f.withTop.toSupHom = f.withTop
                                                                                                                                  @[simp]
                                                                                                                                  theorem LatticeHom.coe_withTop {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] (f : LatticeHom α β) :
                                                                                                                                  f.withTop = WithTop.map f
                                                                                                                                  theorem LatticeHom.withTop_apply {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] (f : LatticeHom α β) (a : WithTop α) :
                                                                                                                                  f.withTop a = WithTop.map (⇑f) a
                                                                                                                                  @[simp]
                                                                                                                                  theorem LatticeHom.withTop_id {α : Type u_3} [Lattice α] :
                                                                                                                                  @[simp]
                                                                                                                                  theorem LatticeHom.withTop_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Lattice α] [Lattice β] [Lattice γ] (f : LatticeHom β γ) (g : LatticeHom α β) :
                                                                                                                                  (f.comp g).withTop = f.withTop.comp g.withTop
                                                                                                                                  def LatticeHom.withBot {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] (f : LatticeHom α β) :

                                                                                                                                  Adjoins a to the domain and codomain of a LatticeHom.

                                                                                                                                  Equations
                                                                                                                                  • f.withBot = { toFun := f.withBot, map_sup' := , map_inf' := }
                                                                                                                                  Instances For
                                                                                                                                    @[simp]
                                                                                                                                    theorem LatticeHom.withBot_toSupHom_toFun {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] (f : LatticeHom α β) (a : WithBot α) :
                                                                                                                                    f.withBot.toSupHom a = f.withBot a
                                                                                                                                    @[simp]
                                                                                                                                    theorem LatticeHom.coe_withBot {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] (f : LatticeHom α β) :
                                                                                                                                    f.withBot = Option.map f
                                                                                                                                    theorem LatticeHom.withBot_apply {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] (f : LatticeHom α β) (a : WithBot α) :
                                                                                                                                    f.withBot a = WithBot.map (⇑f) a
                                                                                                                                    @[simp]
                                                                                                                                    theorem LatticeHom.withBot_id {α : Type u_3} [Lattice α] :
                                                                                                                                    @[simp]
                                                                                                                                    theorem LatticeHom.withBot_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Lattice α] [Lattice β] [Lattice γ] (f : LatticeHom β γ) (g : LatticeHom α β) :
                                                                                                                                    (f.comp g).withBot = f.withBot.comp g.withBot
                                                                                                                                    def LatticeHom.withTopWithBot {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] (f : LatticeHom α β) :

                                                                                                                                    Adjoins a and to the domain and codomain of a LatticeHom.

                                                                                                                                    Equations
                                                                                                                                    • f.withTopWithBot = { toLatticeHom := f.withBot.withTop, map_top' := , map_bot' := }
                                                                                                                                    Instances For
                                                                                                                                      @[simp]
                                                                                                                                      theorem LatticeHom.withTopWithBot_toLatticeHom {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] (f : LatticeHom α β) :
                                                                                                                                      f.withTopWithBot.toLatticeHom = f.withBot.withTop
                                                                                                                                      @[simp]
                                                                                                                                      theorem LatticeHom.coe_withTopWithBot {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] (f : LatticeHom α β) :
                                                                                                                                      f.withTopWithBot = Option.map (Option.map f)
                                                                                                                                      theorem LatticeHom.withTopWithBot_apply {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] (f : LatticeHom α β) (a : WithTop (WithBot α)) :
                                                                                                                                      f.withTopWithBot a = WithTop.map (Option.map f) a
                                                                                                                                      @[simp]
                                                                                                                                      theorem LatticeHom.withTopWithBot_id {α : Type u_3} [Lattice α] :
                                                                                                                                      @[simp]
                                                                                                                                      theorem LatticeHom.withTopWithBot_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Lattice α] [Lattice β] [Lattice γ] (f : LatticeHom β γ) (g : LatticeHom α β) :
                                                                                                                                      (f.comp g).withTopWithBot = f.withTopWithBot.comp g.withTopWithBot
                                                                                                                                      def LatticeHom.withTop' {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] [OrderTop β] (f : LatticeHom α β) :

                                                                                                                                      Adjoins a to the codomain of a LatticeHom.

                                                                                                                                      Equations
                                                                                                                                      • f.withTop' = { toSupHom := f.withTop', map_inf' := }
                                                                                                                                      Instances For
                                                                                                                                        @[simp]
                                                                                                                                        theorem LatticeHom.withTop'_toSupHom {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] [OrderTop β] (f : LatticeHom α β) :
                                                                                                                                        f.withTop'.toSupHom = f.withTop'
                                                                                                                                        def LatticeHom.withBot' {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] [OrderBot β] (f : LatticeHom α β) :

                                                                                                                                        Adjoins a to the domain and codomain of a LatticeHom.

                                                                                                                                        Equations
                                                                                                                                        • f.withBot' = { toSupHom := f.withBot'.toSupHom, map_inf' := }
                                                                                                                                        Instances For
                                                                                                                                          @[simp]
                                                                                                                                          theorem LatticeHom.withBot'_toSupHom {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] [OrderBot β] (f : LatticeHom α β) :
                                                                                                                                          f.withBot'.toSupHom = f.withBot'.toSupHom
                                                                                                                                          def LatticeHom.withTopWithBot' {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] [BoundedOrder β] (f : LatticeHom α β) :

                                                                                                                                          Adjoins a and to the codomain of a LatticeHom.

                                                                                                                                          Equations
                                                                                                                                          • f.withTopWithBot' = { toLatticeHom := f.withBot'.withTop', map_top' := , map_bot' := }
                                                                                                                                          Instances For
                                                                                                                                            @[simp]
                                                                                                                                            theorem LatticeHom.withTopWithBot'_toLatticeHom {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] [BoundedOrder β] (f : LatticeHom α β) :
                                                                                                                                            f.withTopWithBot'.toLatticeHom = f.withBot'.withTop'