# 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 #

• SupHom: Maps which preserve ⊔.
• InfHom: Maps which preserve ⊓.
• SupBotHom: Finitary supremum homomorphisms. Maps which preserve ⊔ and ⊥.
• InfTopHom: Finitary infimum homomorphisms. Maps which preserve ⊓ and ⊤.
• LatticeHom: Lattice homomorphisms. Maps which preserve ⊔ and ⊓.
• BoundedLatticeHom: Bounded lattice homomorphisms. Maps which preserve ⊤, ⊥, ⊔ and ⊓.

## Typeclasses #

• SupHomClass
• InfHomClass
• SupBotHomClass
• InfTopHomClass
• LatticeHomClass
• BoundedLatticeHomClass

## TODO #

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

structure SupHom (α : Type u_7) (β : Type u_8) [Sup α] [Sup β] :
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} [Sup α] [Sup β] (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) [Inf α] [Inf β] :
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} [Inf α] [Inf β] (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) [Sup α] [Sup β] [Bot α] [Bot β] extends :
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} [Sup α] [Sup β] [Bot α] [Bot β] (self : ) :
self.toFun =

A SupBotHom preserves the bottom element.

structure InfTopHom (α : Type u_7) (β : Type u_8) [Inf α] [Inf β] [Top α] [Top β] extends :
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} [Inf α] [Inf β] [Top α] [Top β] (self : ) :
self.toFun =

An InfTopHom preserves the top element.

structure LatticeHom (α : Type u_7) (β : Type u_8) [] [] extends :
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} [] [] (self : ) (a : α) (b : α) :
self.toFun (a b) = self.toFun a self.toFun b

A LatticeHom preserves infima.

structure BoundedLatticeHom (α : Type u_7) (β : Type u_8) [] [] [] [] extends :
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} [] [] [] [] (self : ) :
self.toFun =

A BoundedLatticeHom preserves the top element.

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

A BoundedLatticeHom preserves the bottom element.

class SupHomClass (F : Type u_7) (α : Type u_8) (β : Type u_9) [Sup α] [Sup β] [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} [Sup α] [Sup β] [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) [Inf α] [Inf β] [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} [Inf α] [Inf β] [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) [Sup α] [Sup β] [Bot α] [Bot β] [FunLike F α β] extends :

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} [Sup α] [Sup β] [Bot α] [Bot β] [FunLike F α β] [self : ] (f : F) :

A SupBotHomClass morphism preserves the bottom element.

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

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} [Inf α] [Inf β] [Top α] [Top β] [FunLike F α β] [self : ] (f : F) :

An InfTopHomClass morphism preserves the top element.

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

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} [] [] [FunLike F α β] [self : ] (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) [] [] [] [] [FunLike F α β] extends :

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

You should extend this class when you extend BoundedLatticeHom.

• 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
• map_top : ∀ (f : F), f =

A BoundedLatticeHomClass morphism preserves the top element.

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

A BoundedLatticeHomClass morphism preserves the bottom element.

Instances
theorem BoundedLatticeHomClass.map_top {F : Type u_7} {α : Type u_8} {β : Type u_9} [] [] [] [] [FunLike F α β] [self : ] (f : F) :

A BoundedLatticeHomClass morphism preserves the top element.

theorem BoundedLatticeHomClass.map_bot {F : Type u_7} {α : Type u_8} {β : Type u_9} [] [] [] [] [FunLike F α β] [self : ] (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 α β] [] [] [SupHomClass F α β] :
Equations
• =
@[instance 100]
instance InfHomClass.toOrderHomClass {F : Type u_1} {α : Type u_3} {β : Type u_4} [FunLike F α β] [] [] [InfHomClass F α β] :
Equations
• =
@[instance 100]
instance SupBotHomClass.toBotHomClass {F : Type u_1} {α : Type u_3} {β : Type u_4} [FunLike F α β] [Sup α] [Sup β] [Bot α] [Bot β] [] :
BotHomClass F α β
Equations
• =
@[instance 100]
instance InfTopHomClass.toTopHomClass {F : Type u_1} {α : Type u_3} {β : Type u_4} [FunLike F α β] [Inf α] [Inf β] [Top α] [Top β] [] :
TopHomClass F α β
Equations
• =
@[instance 100]
instance LatticeHomClass.toInfHomClass {F : Type u_1} {α : Type u_3} {β : Type u_4} [FunLike F α β] [] [] [] :
InfHomClass F α β
Equations
• =
@[instance 100]
instance BoundedLatticeHomClass.toSupBotHomClass {F : Type u_1} {α : Type u_3} {β : Type u_4} [FunLike F α β] [] [] [] [] [] :
Equations
• =
@[instance 100]
instance BoundedLatticeHomClass.toInfTopHomClass {F : Type u_1} {α : Type u_3} {β : Type u_4} [FunLike F α β] [] [] [] [] [] :
Equations
• =
@[instance 100]
instance BoundedLatticeHomClass.toBoundedOrderHomClass {F : Type u_1} {α : Type u_3} {β : Type u_4} [FunLike F α β] [] [] [] [] [] :
Equations
• =
@[instance 100]
instance OrderIsoClass.toSupHomClass {F : Type u_1} {α : Type u_3} {β : Type u_4} [EquivLike F α β] [] [] [] :
SupHomClass F α β
Equations
• =
@[instance 100]
instance OrderIsoClass.toInfHomClass {F : Type u_1} {α : Type u_3} {β : Type u_4} [EquivLike F α β] [] [] [] :
InfHomClass F α β
Equations
• =
@[instance 100]
instance OrderIsoClass.toSupBotHomClass {F : Type u_1} {α : Type u_3} {β : Type u_4} [EquivLike F α β] [] [] [] [] [] :
Equations
• =
@[instance 100]
instance OrderIsoClass.toInfTopHomClass {F : Type u_1} {α : Type u_3} {β : Type u_4} [EquivLike F α β] [] [] [] [] [] :
Equations
• =
@[instance 100]
instance OrderIsoClass.toLatticeHomClass {F : Type u_1} {α : Type u_3} {β : Type u_4} [EquivLike F α β] [] [] [] :
Equations
• =
@[instance 100]
instance OrderIsoClass.toBoundedLatticeHomClass {F : Type u_1} {α : Type u_3} {β : Type u_4} [EquivLike F α β] [] [] [] [] [] :
Equations
• =
@[simp]
theorem orderEmbeddingOfInjective_apply {F : Type u_1} {α : Type u_3} {β : Type u_4} [FunLike F α β] [] [] (f : F) [InfHomClass F α β] (hf : ) (a : α) :
a = f a
def orderEmbeddingOfInjective {F : Type u_1} {α : Type u_3} {β : Type u_4} [FunLike F α β] [] [] (f : F) [InfHomClass F α β] (hf : ) :
α ↪o β

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

Equations
Instances For
theorem Disjoint.map {F : Type u_1} {α : Type u_3} {β : Type u_4} [] [] [] [] [FunLike 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} [] [] [] [] [FunLike F α β] [] (f : F) {a : α} {b : α} (h : ) :
Codisjoint (f a) (f b)
theorem IsCompl.map {F : Type u_1} {α : Type u_3} {β : Type u_4} [] [] [] [] [FunLike 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} [] [] [FunLike 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} [] [] [FunLike 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} [] [] [FunLike 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 α β] [Sup α] [Sup β] [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 α β] [Inf α] [Inf β] [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 α β] [Sup α] [Sup β] [Bot α] [Bot β] [] :
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 α β] [Inf α] [Inf β] [Top α] [Top β] [] :
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 α β] [] [] [] :
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 α β] [] [] [] [] [] :
Equations
• One or more equations did not get rendered due to their size.

### Supremum homomorphisms #

instance SupHom.instFunLike {α : Type u_3} {β : Type u_4} [Sup α] [Sup β] :
FunLike (SupHom α β) α β
Equations
• SupHom.instFunLike = { coe := SupHom.toFun, coe_injective' := }
instance SupHom.instSupHomClass {α : Type u_3} {β : Type u_4} [Sup α] [Sup β] :
SupHomClass (SupHom α β) α β
Equations
• =
@[simp]
theorem SupHom.toFun_eq_coe {α : Type u_3} {β : Type u_4} [Sup α] [Sup β] (f : SupHom α β) :
f.toFun = f
@[simp]
theorem SupHom.coe_mk {α : Type u_3} {β : Type u_4} [Sup α] [Sup β] (f : αβ) (hf : ∀ (a b : α), f (a b) = f a f b) :
{ toFun := f, map_sup' := hf } = f
theorem SupHom.ext_iff {α : Type u_3} {β : Type u_4} [Sup α] [Sup β] {f : SupHom α β} {g : SupHom α β} :
f = g ∀ (a : α), f a = g a
theorem SupHom.ext {α : Type u_3} {β : Type u_4} [Sup α] [Sup β] {f : SupHom α β} {g : SupHom α β} (h : ∀ (a : α), f a = g a) :
f = g
def SupHom.copy {α : Type u_3} {β : Type u_4} [Sup α] [Sup β] (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} [Sup α] [Sup β] (f : SupHom α β) (f' : αβ) (h : f' = f) :
(f.copy f' h) = f'
theorem SupHom.copy_eq {α : Type u_3} {β : Type u_4} [Sup α] [Sup β] (f : SupHom α β) (f' : αβ) (h : f' = f) :
f.copy f' h = f
def SupHom.id (α : Type u_3) [Sup α] :
SupHom α α

id as a SupHom.

Equations
• = { toFun := id, map_sup' := }
Instances For
instance SupHom.instInhabited (α : Type u_3) [Sup α] :
Equations
• = { default := }
@[simp]
theorem SupHom.coe_id (α : Type u_3) [Sup α] :
(SupHom.id α) = id
@[simp]
theorem SupHom.id_apply {α : Type u_3} [Sup α] (a : α) :
(SupHom.id α) a = a
def SupHom.comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Sup α] [Sup β] [Sup γ] (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} [Sup α] [Sup β] [Sup γ] (f : SupHom β γ) (g : SupHom α β) :
(f.comp g) = f g
@[simp]
theorem SupHom.comp_apply {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Sup α] [Sup β] [Sup γ] (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} [Sup α] [Sup β] [Sup γ] [Sup δ] (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} [Sup α] [Sup β] (f : SupHom α β) :
f.comp (SupHom.id α) = f
@[simp]
theorem SupHom.id_comp {α : Type u_3} {β : Type u_4} [Sup α] [Sup β] (f : SupHom α β) :
(SupHom.id β).comp f = f
@[simp]
theorem SupHom.cancel_right {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Sup α] [Sup β] [Sup γ] {g₁ : SupHom β γ} {g₂ : SupHom β γ} {f : SupHom α β} (hf : ) :
g₁.comp f = g₂.comp f g₁ = g₂
@[simp]
theorem SupHom.cancel_left {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Sup α] [Sup β] [Sup γ] {g : SupHom β γ} {f₁ : SupHom α β} {f₂ : SupHom α β} (hg : ) :
g.comp f₁ = g.comp f₂ f₁ = f₂
def SupHom.const (α : Type u_3) {β : Type u_4} [Sup α] [] (b : β) :
SupHom α β

The constant function as a SupHom.

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

Subtype.val as a SupHom.

Equations
• = { toFun := Subtype.val, map_sup' := }
Instances For
@[simp]
theorem SupHom.subtypeVal_apply {β : Type u_4} [] {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} [] {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} [Inf α] [Inf β] :
FunLike (InfHom α β) α β
Equations
• InfHom.instFunLike = { coe := InfHom.toFun, coe_injective' := }
instance InfHom.instInfHomClass {α : Type u_3} {β : Type u_4} [Inf α] [Inf β] :
InfHomClass (InfHom α β) α β
Equations
• =
@[simp]
theorem InfHom.toFun_eq_coe {α : Type u_3} {β : Type u_4} [Inf α] [Inf β] (f : InfHom α β) :
f.toFun = f
@[simp]
theorem InfHom.coe_mk {α : Type u_3} {β : Type u_4} [Inf α] [Inf β] (f : αβ) (hf : ∀ (a b : α), f (a b) = f a f b) :
{ toFun := f, map_inf' := hf } = f
theorem InfHom.ext_iff {α : Type u_3} {β : Type u_4} [Inf α] [Inf β] {f : InfHom α β} {g : InfHom α β} :
f = g ∀ (a : α), f a = g a
theorem InfHom.ext {α : Type u_3} {β : Type u_4} [Inf α] [Inf β] {f : InfHom α β} {g : InfHom α β} (h : ∀ (a : α), f a = g a) :
f = g
def InfHom.copy {α : Type u_3} {β : Type u_4} [Inf α] [Inf β] (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} [Inf α] [Inf β] (f : InfHom α β) (f' : αβ) (h : f' = f) :
(f.copy f' h) = f'
theorem InfHom.copy_eq {α : Type u_3} {β : Type u_4} [Inf α] [Inf β] (f : InfHom α β) (f' : αβ) (h : f' = f) :
f.copy f' h = f
def InfHom.id (α : Type u_3) [Inf α] :
InfHom α α

id as an InfHom.

Equations
• = { toFun := id, map_inf' := }
Instances For
instance InfHom.instInhabited (α : Type u_3) [Inf α] :
Equations
• = { default := }
@[simp]
theorem InfHom.coe_id (α : Type u_3) [Inf α] :
(InfHom.id α) = id
@[simp]
theorem InfHom.id_apply {α : Type u_3} [Inf α] (a : α) :
(InfHom.id α) a = a
def InfHom.comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Inf α] [Inf β] [Inf γ] (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} [Inf α] [Inf β] [Inf γ] (f : InfHom β γ) (g : InfHom α β) :
(f.comp g) = f g
@[simp]
theorem InfHom.comp_apply {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Inf α] [Inf β] [Inf γ] (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} [Inf α] [Inf β] [Inf γ] [Inf δ] (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} [Inf α] [Inf β] (f : InfHom α β) :
f.comp (InfHom.id α) = f
@[simp]
theorem InfHom.id_comp {α : Type u_3} {β : Type u_4} [Inf α] [Inf β] (f : InfHom α β) :
(InfHom.id β).comp f = f
@[simp]
theorem InfHom.cancel_right {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Inf α] [Inf β] [Inf γ] {g₁ : InfHom β γ} {g₂ : InfHom β γ} {f : InfHom α β} (hf : ) :
g₁.comp f = g₂.comp f g₁ = g₂
@[simp]
theorem InfHom.cancel_left {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Inf α] [Inf β] [Inf γ] {g : InfHom β γ} {f₁ : InfHom α β} {f₂ : InfHom α β} (hg : ) :
g.comp f₁ = g.comp f₂ f₁ = f₂
def InfHom.const (α : Type u_3) {β : Type u_4} [Inf α] [] (b : β) :
InfHom α β

The constant function as an InfHom.

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

Subtype.val as an InfHom.

Equations
• = { toFun := Subtype.val, map_inf' := }
Instances For
@[simp]
theorem InfHom.subtypeVal_apply {β : Type u_4} [] {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} [] {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} [Sup α] [Bot α] [Sup β] [Bot β] (f : ) :
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} [Sup α] [Bot α] [Sup β] [Bot β] :
FunLike (SupBotHom α β) α β
Equations
• SupBotHom.instFunLike = { coe := fun (f : ) => f.toFun, coe_injective' := }
instance SupBotHom.instSupBotHomClass {α : Type u_3} {β : Type u_4} [Sup α] [Bot α] [Sup β] [Bot β] :
Equations
• =
theorem SupBotHom.toFun_eq_coe {α : Type u_3} {β : Type u_4} [Sup α] [Bot α] [Sup β] [Bot β] (f : ) :
f.toFun = f
@[simp]
theorem SupBotHom.coe_toSupHom {α : Type u_3} {β : Type u_4} [Sup α] [Bot α] [Sup β] [Bot β] (f : ) :
f.toSupHom = f
@[simp]
theorem SupBotHom.coe_toBotHom {α : Type u_3} {β : Type u_4} [Sup α] [Bot α] [Sup β] [Bot β] (f : ) :
f.toBotHom = f
@[simp]
theorem SupBotHom.coe_mk {α : Type u_3} {β : Type u_4} [Sup α] [Bot α] [Sup β] [Bot β] (f : SupHom α β) (hf : f.toFun = ) :
{ toSupHom := f, map_bot' := hf } = f
theorem SupBotHom.ext_iff {α : Type u_3} {β : Type u_4} [Sup α] [Bot α] [Sup β] [Bot β] {f : } {g : } :
f = g ∀ (a : α), f a = g a
theorem SupBotHom.ext {α : Type u_3} {β : Type u_4} [Sup α] [Bot α] [Sup β] [Bot β] {f : } {g : } (h : ∀ (a : α), f a = g a) :
f = g
def SupBotHom.copy {α : Type u_3} {β : Type u_4} [Sup α] [Bot α] [Sup β] [Bot β] (f : ) (f' : αβ) (h : f' = f) :

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} [Sup α] [Bot α] [Sup β] [Bot β] (f : ) (f' : αβ) (h : f' = f) :
(f.copy f' h) = f'
theorem SupBotHom.copy_eq {α : Type u_3} {β : Type u_4} [Sup α] [Bot α] [Sup β] [Bot β] (f : ) (f' : αβ) (h : f' = f) :
f.copy f' h = f
@[simp]
theorem SupBotHom.id_toSupHom (α : Type u_3) [Sup α] [Bot α] :
(SupBotHom.id α).toSupHom =
def SupBotHom.id (α : Type u_3) [Sup α] [Bot α] :

id as a SupBotHom.

Equations
• = { toSupHom := , map_bot' := }
Instances For
instance SupBotHom.instInhabited (α : Type u_3) [Sup α] [Bot α] :
Equations
• = { default := }
@[simp]
theorem SupBotHom.coe_id (α : Type u_3) [Sup α] [Bot α] :
(SupBotHom.id α) = id
@[simp]
theorem SupBotHom.id_apply {α : Type u_3} [Sup α] [Bot α] (a : α) :
(SupBotHom.id α) a = a
def SupBotHom.comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Sup α] [Bot α] [Sup β] [Bot β] [Sup γ] [Bot γ] (f : ) (g : ) :

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} [Sup α] [Bot α] [Sup β] [Bot β] [Sup γ] [Bot γ] (f : ) (g : ) :
(f.comp g) = f g
@[simp]
theorem SupBotHom.comp_apply {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Sup α] [Bot α] [Sup β] [Bot β] [Sup γ] [Bot γ] (f : ) (g : ) (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} [Sup α] [Bot α] [Sup β] [Bot β] [Sup γ] [Bot γ] [Sup δ] [Bot δ] (f : ) (g : ) (h : ) :
(f.comp g).comp h = f.comp (g.comp h)
@[simp]
theorem SupBotHom.comp_id {α : Type u_3} {β : Type u_4} [Sup α] [Bot α] [Sup β] [Bot β] (f : ) :
f.comp (SupBotHom.id α) = f
@[simp]
theorem SupBotHom.id_comp {α : Type u_3} {β : Type u_4} [Sup α] [Bot α] [Sup β] [Bot β] (f : ) :
(SupBotHom.id β).comp f = f
@[simp]
theorem SupBotHom.cancel_right {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Sup α] [Bot α] [Sup β] [Bot β] [Sup γ] [Bot γ] {g₁ : } {g₂ : } {f : } (hf : ) :
g₁.comp f = g₂.comp f g₁ = g₂
@[simp]
theorem SupBotHom.cancel_left {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Sup α] [Bot α] [Sup β] [Bot β] [Sup γ] [Bot γ] {g : } {f₁ : } {f₂ : } (hg : ) :
g.comp f₁ = g.comp f₂ f₁ = f₂
instance SupBotHom.instSup {α : Type u_3} {β : Type u_4} [Sup α] [Bot α] [] [] :
Sup (SupBotHom α β)
Equations
• SupBotHom.instSup = { sup := fun (f g : ) => let __src := f.toBotHom g.toBotHom; { toSupHom := f.toSupHom g.toSupHom, map_bot' := } }
instance SupBotHom.instSemilatticeSup {α : Type u_3} {β : Type u_4} [Sup α] [Bot α] [] [] :
Equations
instance SupBotHom.instOrderBot {α : Type u_3} {β : Type u_4} [Sup α] [Bot α] [] [] :
Equations
• SupBotHom.instOrderBot =
@[simp]
theorem SupBotHom.coe_sup {α : Type u_3} {β : Type u_4} [Sup α] [Bot α] [] [] (f : ) (g : ) :
(f g) = (f g)
@[simp]
theorem SupBotHom.coe_bot {α : Type u_3} {β : Type u_4} [Sup α] [Bot α] [] [] :
=
@[simp]
theorem SupBotHom.sup_apply {α : Type u_3} {β : Type u_4} [Sup α] [Bot α] [] [] (f : ) (g : ) (a : α) :
(f g) a = f a g a
@[simp]
theorem SupBotHom.bot_apply {α : Type u_3} {β : Type u_4} [Sup α] [Bot α] [] [] (a : α) :
def SupBotHom.subtypeVal {β : Type u_4} [] [] {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} [] [] {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} [] [] {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} [Inf α] [Top α] [Inf β] [Top β] (f : ) :
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} [Inf α] [Top α] [Inf β] [Top β] :
FunLike (InfTopHom α β) α β
Equations
• InfTopHom.instFunLike = { coe := fun (f : ) => f.toFun, coe_injective' := }
instance InfTopHom.instInfTopHomClass {α : Type u_3} {β : Type u_4} [Inf α] [Top α] [Inf β] [Top β] :
Equations
• =
theorem InfTopHom.toFun_eq_coe {α : Type u_3} {β : Type u_4} [Inf α] [Top α] [Inf β] [Top β] (f : ) :
f.toFun = f
@[simp]
theorem InfTopHom.coe_toInfHom {α : Type u_3} {β : Type u_4} [Inf α] [Top α] [Inf β] [Top β] (f : ) :
f.toInfHom = f
@[simp]
theorem InfTopHom.coe_toTopHom {α : Type u_3} {β : Type u_4} [Inf α] [Top α] [Inf β] [Top β] (f : ) :
f.toTopHom = f
@[simp]
theorem InfTopHom.coe_mk {α : Type u_3} {β : Type u_4} [Inf α] [Top α] [Inf β] [Top β] (f : InfHom α β) (hf : f.toFun = ) :
{ toInfHom := f, map_top' := hf } = f
theorem InfTopHom.ext_iff {α : Type u_3} {β : Type u_4} [Inf α] [Top α] [Inf β] [Top β] {f : } {g : } :
f = g ∀ (a : α), f a = g a
theorem InfTopHom.ext {α : Type u_3} {β : Type u_4} [Inf α] [Top α] [Inf β] [Top β] {f : } {g : } (h : ∀ (a : α), f a = g a) :
f = g
def InfTopHom.copy {α : Type u_3} {β : Type u_4} [Inf α] [Top α] [Inf β] [Top β] (f : ) (f' : αβ) (h : f' = f) :

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} [Inf α] [Top α] [Inf β] [Top β] (f : ) (f' : αβ) (h : f' = f) :
(f.copy f' h) = f'
theorem InfTopHom.copy_eq {α : Type u_3} {β : Type u_4} [Inf α] [Top α] [Inf β] [Top β] (f : ) (f' : αβ) (h : f' = f) :
f.copy f' h = f
@[simp]
theorem InfTopHom.id_toInfHom (α : Type u_3) [Inf α] [Top α] :
(InfTopHom.id α).toInfHom =
def InfTopHom.id (α : Type u_3) [Inf α] [Top α] :

id as an InfTopHom.

Equations
• = { toInfHom := , map_top' := }
Instances For
instance InfTopHom.instInhabited (α : Type u_3) [Inf α] [Top α] :
Equations
• = { default := }
@[simp]
theorem InfTopHom.coe_id (α : Type u_3) [Inf α] [Top α] :
(InfTopHom.id α) = id
@[simp]
theorem InfTopHom.id_apply {α : Type u_3} [Inf α] [Top α] (a : α) :
(InfTopHom.id α) a = a
def InfTopHom.comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Inf α] [Top α] [Inf β] [Top β] [Inf γ] [Top γ] (f : ) (g : ) :

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} [Inf α] [Top α] [Inf β] [Top β] [Inf γ] [Top γ] (f : ) (g : ) :
(f.comp g) = f g
@[simp]
theorem InfTopHom.comp_apply {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Inf α] [Top α] [Inf β] [Top β] [Inf γ] [Top γ] (f : ) (g : ) (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} [Inf α] [Top α] [Inf β] [Top β] [Inf γ] [Top γ] [Inf δ] [Top δ] (f : ) (g : ) (h : ) :
(f.comp g).comp h = f.comp (g.comp h)
@[simp]
theorem InfTopHom.comp_id {α : Type u_3} {β : Type u_4} [Inf α] [Top α] [Inf β] [Top β] (f : ) :
f.comp (InfTopHom.id α) = f
@[simp]
theorem InfTopHom.id_comp {α : Type u_3} {β : Type u_4} [Inf α] [Top α] [Inf β] [Top β] (f : ) :
(InfTopHom.id β).comp f = f
@[simp]
theorem InfTopHom.cancel_right {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Inf α] [Top α] [Inf β] [Top β] [Inf γ] [Top γ] {g₁ : } {g₂ : } {f : } (hf : ) :
g₁.comp f = g₂.comp f g₁ = g₂
@[simp]
theorem InfTopHom.cancel_left {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Inf α] [Top α] [Inf β] [Top β] [Inf γ] [Top γ] {g : } {f₁ : } {f₂ : } (hg : ) :
g.comp f₁ = g.comp f₂ f₁ = f₂
instance InfTopHom.instInf {α : Type u_3} {β : Type u_4} [Inf α] [Top α] [] [] :
Inf (InfTopHom α β)
Equations
• InfTopHom.instInf = { inf := fun (f g : ) => let __src := f.toTopHom g.toTopHom; { toInfHom := f.toInfHom g.toInfHom, map_top' := } }
instance InfTopHom.instSemilatticeInf {α : Type u_3} {β : Type u_4} [Inf α] [Top α] [] [] :
Equations
instance InfTopHom.instOrderTop {α : Type u_3} {β : Type u_4} [Inf α] [Top α] [] [] :
Equations
• InfTopHom.instOrderTop =
@[simp]
theorem InfTopHom.coe_inf {α : Type u_3} {β : Type u_4} [Inf α] [Top α] [] [] (f : ) (g : ) :
(f g) = (f g)
@[simp]
theorem InfTopHom.coe_top {α : Type u_3} {β : Type u_4} [Inf α] [Top α] [] [] :
=
@[simp]
theorem InfTopHom.inf_apply {α : Type u_3} {β : Type u_4} [Inf α] [Top α] [] [] (f : ) (g : ) (a : α) :
(f g) a = f a g a
@[simp]
theorem InfTopHom.top_apply {α : Type u_3} {β : Type u_4} [Inf α] [Top α] [] [] (a : α) :
def InfTopHom.subtypeVal {β : Type u_4} [] [] {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} [] [] {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} [] [] {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} [] [] (f : ) :
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} [] [] :
FunLike (LatticeHom α β) α β
Equations
• LatticeHom.instFunLike = { coe := fun (f : ) => f.toFun, coe_injective' := }
instance LatticeHom.instLatticeHomClass {α : Type u_3} {β : Type u_4} [] [] :
Equations
• =
theorem LatticeHom.toFun_eq_coe {α : Type u_3} {β : Type u_4} [] [] (f : ) :
f.toFun = f
@[simp]
theorem LatticeHom.coe_toSupHom {α : Type u_3} {β : Type u_4} [] [] (f : ) :
f.toSupHom = f
@[simp]
theorem LatticeHom.coe_toInfHom {α : Type u_3} {β : Type u_4} [] [] (f : ) :
f.toInfHom = f
@[simp]
theorem LatticeHom.coe_mk {α : Type u_3} {β : Type u_4} [] [] (f : SupHom α β) (hf : ∀ (a b : α), f.toFun (a b) = f.toFun a f.toFun b) :
{ toSupHom := f, map_inf' := hf } = f
theorem LatticeHom.ext_iff {α : Type u_3} {β : Type u_4} [] [] {f : } {g : } :
f = g ∀ (a : α), f a = g a
theorem LatticeHom.ext {α : Type u_3} {β : Type u_4} [] [] {f : } {g : } (h : ∀ (a : α), f a = g a) :
f = g
def LatticeHom.copy {α : Type u_3} {β : Type u_4} [] [] (f : ) (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} [] [] (f : ) (f' : αβ) (h : f' = f) :
(f.copy f' h) = f'
theorem LatticeHom.copy_eq {α : Type u_3} {β : Type u_4} [] [] (f : ) (f' : αβ) (h : f' = f) :
f.copy f' h = f
def LatticeHom.id (α : Type u_3) [] :

id as a LatticeHom.

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

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} [] [] [] (f : ) (g : ) :
(f.comp g) = f g
@[simp]
theorem LatticeHom.comp_apply {α : Type u_3} {β : Type u_4} {γ : Type u_5} [] [] [] (f : ) (g : ) (a : α) :
(f.comp g) a = f (g a)
@[simp]
theorem LatticeHom.coe_comp_sup_hom' {α : Type u_3} {β : Type u_4} {γ : Type u_5} [] [] [] (f : ) (g : ) :
{ 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} [] [] [] (f : ) (g : ) :
{ 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} [] [] [] (f : ) (g : ) :
{ 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} [] [] [] (f : ) (g : ) :
{ 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} [] [] [] [] (f : ) (g : ) (h : ) :
(f.comp g).comp h = f.comp (g.comp h)
@[simp]
theorem LatticeHom.comp_id {α : Type u_3} {β : Type u_4} [] [] (f : ) :
f.comp = f
@[simp]
theorem LatticeHom.id_comp {α : Type u_3} {β : Type u_4} [] [] (f : ) :
.comp f = f
@[simp]
theorem LatticeHom.cancel_right {α : Type u_3} {β : Type u_4} {γ : Type u_5} [] [] [] {g₁ : } {g₂ : } {f : } (hf : ) :
g₁.comp f = g₂.comp f g₁ = g₂
@[simp]
theorem LatticeHom.cancel_left {α : Type u_3} {β : Type u_4} {γ : Type u_5} [] [] [] {g : } {f₁ : } {f₂ : } (hg : ) :
g.comp f₁ = g.comp f₂ f₁ = f₂
def LatticeHom.subtypeVal {β : Type u_4} [] {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} [] {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} [] {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 α β] [] [] [] :

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 α β] [] [] [] (f : F) :

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

Equations
• = { toFun := f, map_sup' := , map_inf' := }
Instances For
@[simp]
theorem OrderHomClass.coe_to_lattice_hom {F : Type u_1} (α : Type u_3) (β : Type u_4) [FunLike F α β] [] [] [] (f : F) :
= f
@[simp]
theorem OrderHomClass.to_lattice_hom_apply {F : Type u_1} (α : Type u_3) (β : Type u_4) [FunLike F α β] [] [] [] (f : F) (a : α) :
a = f a

### Bounded lattice homomorphisms #

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

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} [] [] [] [] (f : ) :

Reinterpret a BoundedLatticeHom as an InfTopHom.

Equations
• f.toInfTopHom = { toFun := f.toFun, map_inf' := , map_top' := }
Instances For
def BoundedLatticeHom.toBoundedOrderHom {α : Type u_3} {β : Type u_4} [] [] [] [] (f : ) :

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} [] [] [] [] :
FunLike α β
Equations
• BoundedLatticeHom.instFunLike = { coe := fun (f : ) => f.toFun, coe_injective' := }
instance BoundedLatticeHom.instBoundedLatticeHomClass {α : Type u_3} {β : Type u_4} [] [] [] [] :
Equations
• =
@[simp]
theorem BoundedLatticeHom.toFun_eq_coe {α : Type u_3} {β : Type u_4} [] [] [] [] (f : ) :
f.toFun = f
@[simp]
theorem BoundedLatticeHom.coe_toLatticeHom {α : Type u_3} {β : Type u_4} [] [] [] [] (f : ) :
f.toLatticeHom = f
@[simp]
theorem BoundedLatticeHom.coe_toSupBotHom {α : Type u_3} {β : Type u_4} [] [] [] [] (f : ) :
f.toSupBotHom = f
@[simp]
theorem BoundedLatticeHom.coe_toInfTopHom {α : Type u_3} {β : Type u_4} [] [] [] [] (f : ) :
f.toInfTopHom = f
@[simp]
theorem BoundedLatticeHom.coe_toBoundedOrderHom {α : Type u_3} {β : Type u_4} [] [] [] [] (f : ) :
f.toBoundedOrderHom = f
@[simp]
theorem BoundedLatticeHom.coe_mk {α : Type u_3} {β : Type u_4} [] [] [] [] (f : ) (hf : f.toFun = ) (hf' : f.toFun = ) :
{ toLatticeHom := f, map_top' := hf, map_bot' := hf' } = f
theorem BoundedLatticeHom.ext_iff {α : Type u_3} {β : Type u_4} [] [] [] [] {f : } {g : } :
f = g ∀ (a : α), f a = g a
theorem BoundedLatticeHom.ext {α : Type u_3} {β : Type u_4} [] [] [] [] {f : } {g : } (h : ∀ (a : α), f a = g a) :
f = g
def BoundedLatticeHom.copy {α : Type u_3} {β : Type u_4} [] [] [] [] (f : ) (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} [] [] [] [] (f : ) (f' : αβ) (h : f' = f) :
(f.copy f' h) = f'
theorem BoundedLatticeHom.copy_eq {α : Type u_3} {β : Type u_4} [] [] [] [] (f : ) (f' : αβ) (h : f' = f) :
f.copy f' h = f
def BoundedLatticeHom.id (α : Type u_3) [] [] :

id as a BoundedLatticeHom.

Equations
• = { toLatticeHom := , map_top' := , map_bot' := }
Instances For
instance BoundedLatticeHom.instInhabited (α : Type u_3) [] [] :
Equations
• = { default := }
@[simp]
theorem BoundedLatticeHom.coe_id (α : Type u_3) [] [] :
= id
@[simp]
theorem BoundedLatticeHom.id_apply {α : Type u_3} [] [] (a : α) :
a = a
def BoundedLatticeHom.comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [] [] [] [] [] [] (f : ) (g : ) :

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} [] [] [] [] [] [] (f : ) (g : ) :
(f.comp g) = f g
@[simp]
theorem BoundedLatticeHom.comp_apply {α : Type u_3} {β : Type u_4} {γ : Type u_5} [] [] [] [] [] [] (f : ) (g : ) (a : α) :
(f.comp g) a = f (g a)
@[simp]
theorem BoundedLatticeHom.coe_comp_lattice_hom' {α : Type u_3} {β : Type u_4} {γ : Type u_5} [] [] [] [] [] [] (f : ) (g : ) :
{ 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} [] [] [] [] [] [] (f : ) (g : ) :
{ 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} [] [] [] [] [] [] (f : ) (g : ) :
{ 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} [] [] [] [] [] [] (f : ) (g : ) :
{ 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} [] [] [] [] [] [] (f : ) (g : ) :
{ 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} [] [] [] [] [] [] (f : ) (g : ) :
{ 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} [] [] [] [] [] [] [] [] (f : ) (g : ) (h : ) :
(f.comp g).comp h = f.comp (g.comp h)
@[simp]
theorem BoundedLatticeHom.comp_id {α : Type u_3} {β : Type u_4} [] [] [] [] (f : ) :
f.comp = f
@[simp]
theorem BoundedLatticeHom.id_comp {α : Type u_3} {β : Type u_4} [] [] [] [] (f : ) :
.comp f = f
@[simp]
theorem BoundedLatticeHom.cancel_right {α : Type u_3} {β : Type u_4} {γ : Type u_5} [] [] [] [] [] [] {g₁ : } {g₂ : } {f : } (hf : ) :
g₁.comp f = g₂.comp f g₁ = g₂
@[simp]
theorem BoundedLatticeHom.cancel_left {α : Type u_3} {β : Type u_4} {γ : Type u_5} [] [] [] [] [] [] {g : } {f₁ : } {f₂ : } (hg : ) :
g.comp f₁ = g.comp f₂ f₁ = f₂
def BoundedLatticeHom.subtypeVal {β : Type u_4} [] [] {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} [] [] {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} [] [] {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 #

@[simp]
theorem SupHom.dual_symm_apply_toFun {α : Type u_3} {β : Type u_4} [Sup α] [Sup β] (f : ) (a : αᵒᵈ) :
(SupHom.dual.symm f) a = f a
@[simp]
theorem SupHom.dual_apply_toFun {α : Type u_3} {β : Type u_4} [Sup α] [Sup β] (f : SupHom α β) (a : α) :
(SupHom.dual f) a = f a
def SupHom.dual {α : Type u_3} {β : Type u_4} [Sup α] [Sup β] :
SupHom α β

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 : ) => { toFun := f, map_sup' := }, left_inv := , right_inv := }
Instances For
@[simp]
theorem SupHom.dual_id {α : Type u_3} [Sup α] :
SupHom.dual (SupHom.id α) =
@[simp]
theorem SupHom.dual_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Sup α] [Sup β] [Sup γ] (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} [Sup α] :
SupHom.dual.symm (InfHom.id αᵒᵈ) =
@[simp]
theorem SupHom.symm_dual_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Sup α] [Sup β] [Sup γ] (g : ) (f : ) :
SupHom.dual.symm (g.comp f) = (SupHom.dual.symm g).comp (SupHom.dual.symm f)
@[simp]
theorem InfHom.dual_apply_toFun {α : Type u_3} {β : Type u_4} [Inf α] [Inf β] (f : InfHom α β) (a : α) :
(InfHom.dual f) a = f a
@[simp]
theorem InfHom.dual_symm_apply_toFun {α : Type u_3} {β : Type u_4} [Inf α] [Inf β] (f : ) (a : αᵒᵈ) :
(InfHom.dual.symm f) a = f a
def InfHom.dual {α : Type u_3} {β : Type u_4} [Inf α] [Inf β] :
InfHom α β

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 : ) => { toFun := f, map_inf' := }, left_inv := , right_inv := }
Instances For
@[simp]
theorem InfHom.dual_id {α : Type u_3} [Inf α] :
InfHom.dual (InfHom.id α) =
@[simp]
theorem InfHom.dual_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Inf α] [Inf β] [Inf γ] (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} [Inf α] :
InfHom.dual.symm (SupHom.id αᵒᵈ) =
@[simp]
theorem InfHom.symm_dual_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Inf α] [Inf β] [Inf γ] (g : ) (f : ) :
InfHom.dual.symm (g.comp f) = (InfHom.dual.symm g).comp (InfHom.dual.symm f)
def SupBotHom.dual {α : Type u_3} {β : Type u_4} [Sup α] [Bot α] [Sup β] [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} [Sup α] [Bot α] :
SupBotHom.dual (SupBotHom.id α) =
@[simp]
theorem SupBotHom.dual_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Sup α] [Bot α] [Sup β] [Bot β] [Sup γ] [Bot γ] (g : ) (f : ) :
SupBotHom.dual (g.comp f) = (SupBotHom.dual g).comp (SupBotHom.dual f)
@[simp]
theorem SupBotHom.symm_dual_id {α : Type u_3} [Sup α] [Bot α] :
SupBotHom.dual.symm =
@[simp]
theorem SupBotHom.symm_dual_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Sup α] [Bot α] [Sup β] [Bot β] [Sup γ] [Bot γ] (g : ) (f : ) :
SupBotHom.dual.symm (g.comp f) = (SupBotHom.dual.symm g).comp (SupBotHom.dual.symm f)
@[simp]
theorem InfTopHom.dual_apply_toSupHom {α : Type u_3} {β : Type u_4} [Inf α] [Top α] [Inf β] [Top β] (f : ) :
(InfTopHom.dual f).toSupHom = InfHom.dual f.toInfHom
@[simp]
theorem InfTopHom.dual_symm_apply_toInfHom {α : Type u_3} {β : Type u_4} [Inf α] [Top α] [Inf β] [Top β] (f : ) :
(InfTopHom.dual.symm f).toInfHom = InfHom.dual.symm f.toSupHom
def InfTopHom.dual {α : Type u_3} {β : Type u_4} [Inf α] [Top α] [Inf β] [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_id {α : Type u_3} [Inf α] [Top α] :
InfTopHom.dual (InfTopHom.id α) =
@[simp]
theorem InfTopHom.dual_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Inf α] [Top α] [Inf β] [Top β] [Inf γ] [Top γ] (g : ) (f : ) :
InfTopHom.dual (g.comp f) = (InfTopHom.dual g).comp (InfTopHom.dual f)
@[simp]
theorem InfTopHom.symm_dual_id {α : Type u_3} [Inf α] [Top α] :
InfTopHom.dual.symm =
@[simp]
theorem InfTopHom.symm_dual_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Inf α] [Top α] [Inf β] [Top β] [Inf γ] [Top γ] (g : ) (f : ) :
InfTopHom.dual.symm (g.comp f) = (InfTopHom.dual.symm g).comp (InfTopHom.dual.symm f)
@[simp]
theorem LatticeHom.dual_symm_apply_toSupHom {α : Type u_3} {β : Type u_4} [] [] (f : ) :
(LatticeHom.dual.symm f).toSupHom = SupHom.dual.symm f.toInfHom
@[simp]
theorem LatticeHom.dual_apply_toSupHom {α : Type u_3} {β : Type u_4} [] [] (f : ) :
(LatticeHom.dual f).toSupHom = InfHom.dual f.toInfHom
def LatticeHom.dual {α : Type u_3} {β : Type u_4} [] [] :

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_id {α : Type u_3} [] :
LatticeHom.dual =
@[simp]
theorem LatticeHom.dual_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [] [] [] (g : ) (f : ) :
LatticeHom.dual (g.comp f) = (LatticeHom.dual g).comp (LatticeHom.dual f)
@[simp]
theorem LatticeHom.symm_dual_id {α : Type u_3} [] :
LatticeHom.dual.symm =
@[simp]
theorem LatticeHom.symm_dual_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [] [] [] (g : ) (f : ) :
LatticeHom.dual.symm (g.comp f) = (LatticeHom.dual.symm g).comp (LatticeHom.dual.symm f)
@[simp]
theorem BoundedLatticeHom.dual_apply_toLatticeHom {α : Type u_3} {β : Type u_4} [] [] [] [] (f : ) :
(BoundedLatticeHom.dual f).toLatticeHom = LatticeHom.dual f.toLatticeHom
@[simp]
theorem BoundedLatticeHom.dual_symm_apply_toLatticeHom {α : Type u_3} {β : Type u_4} [] [] [] [] (f : ) :
(BoundedLatticeHom.dual.symm f).toLatticeHom = LatticeHom.dual.symm f.toLatticeHom
def BoundedLatticeHom.dual {α : Type u_3} {β : Type u_4} [] [] [] [] :

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_id {α : Type u_3} [] [] :
BoundedLatticeHom.dual =
@[simp]
theorem BoundedLatticeHom.dual_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [] [] [] [] [] [] (g : ) (f : ) :
BoundedLatticeHom.dual (g.comp f) = (BoundedLatticeHom.dual g).comp (BoundedLatticeHom.dual f)
@[simp]
theorem BoundedLatticeHom.symm_dual_id {α : Type u_3} [] [] :
BoundedLatticeHom.dual.symm =
@[simp]
theorem BoundedLatticeHom.symm_dual_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [] [] [] [] [] [] (g : ) (f : ) :
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} [] [] :
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} [] [] :
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} [] [] :
LatticeHom.fst = Prod.fst
@[simp]
theorem LatticeHom.coe_snd {α : Type u_3} {β : Type u_4} [] [] :
LatticeHom.snd = Prod.snd
theorem LatticeHom.fst_apply {α : Type u_3} {β : Type u_4} [] [] (x : α × β) :
LatticeHom.fst x = x.1
theorem LatticeHom.snd_apply {α : Type u_3} {β : Type u_4} [] [] (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
• = { toFun := , map_sup' := , map_inf' := }
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) :
f = f i

### WithTop, WithBot#

@[simp]
theorem SupHom.withTop_toFun {α : Type u_3} {β : Type u_4} [] [] (f : SupHom α β) :
∀ (a : ), f.withTop a = WithTop.map (⇑f) a
def SupHom.withTop {α : Type u_3} {β : Type u_4} [] [] (f : SupHom α β) :

Adjoins a ⊤ to the domain and codomain of a SupHom.

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

Adjoins a ⊥ to the domain and codomain of a SupHom.

Equations
• f.withBot = { toFun := , map_sup' := , map_bot' := }
Instances For
@[simp]
theorem SupHom.withBot_id {α : Type u_3} [] :
(SupHom.id α).withBot =
@[simp]
theorem SupHom.withBot_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [] [] [] (f : SupHom β γ) (g : SupHom α β) :
(f.comp g).withBot = f.withBot.comp g.withBot
@[simp]
theorem SupHom.withTop'_toFun {α : Type u_3} {β : Type u_4} [] [] [] (f : SupHom α β) (a : ) :
f.withTop' a = Option.elim a f
def SupHom.withTop' {α : Type u_3} {β : Type u_4} [] [] [] (f : SupHom α β) :
SupHom (WithTop α) β

Adjoins a ⊤ to the codomain of a SupHom.

Equations
• f.withTop' = { toFun := fun (a : ) => Option.elim a f, map_sup' := }
Instances For
@[simp]
theorem SupHom.withBot'_toSupHom_toFun {α : Type u_3} {β : Type u_4} [] [] [] (f : SupHom α β) (a : ) :
f.withBot'.toSupHom a = Option.elim a f
def SupHom.withBot' {α : Type u_3} {β : Type u_4} [] [] [] (f : SupHom α β) :

Adjoins a ⊥ to the domain of a SupHom.

Equations
• f.withBot' = { toFun := fun (a : ) => Option.elim a f, map_sup' := , map_bot' := }
Instances For
@[simp]
theorem InfHom.withTop_toInfHom_toFun {α : Type u_3} {β : Type u_4} [] [] (f : InfHom α β) :
∀ (a : ), f.withTop.toInfHom a = Option.map (⇑f) a
def InfHom.withTop {α : Type u_3} {β : Type u_4} [] [] (f : InfHom α β) :

Adjoins a ⊤ to the domain and codomain of an InfHom.

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

Adjoins a ⊥ to the domain and codomain of an InfHom.

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

Adjoins a ⊤ to the codomain of an InfHom.

Equations
• f.withTop' = { toFun := fun (a : ) => Option.elim a f, map_inf' := , map_top' := }
Instances For
@[simp]
theorem InfHom.withBot'_toFun {α : Type u_3} {β : Type u_4} [] [] [] (f : InfHom α β) (a : ) :
f.withBot' a = Option.elim a f
def InfHom.withBot' {α : Type u_3} {β : Type u_4} [] [] [] (f : InfHom α β) :
InfHom (WithBot α) β

Adjoins a ⊥ to the codomain of an InfHom.

Equations
• f.withBot' = { toFun := fun (a : ) => Option.elim a f, map_inf' := }
Instances For
@[simp]
theorem LatticeHom.withTop_toSupHom {α : Type u_3} {β : Type u_4} [] [] (f : ) :
f.withTop.toSupHom = f.withTop
def LatticeHom.withTop {α : Type u_3} {β : Type u_4} [] [] (f : ) :

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

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

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.coe_withBot {α : Type u_3} {β : Type u_4} [] [] (f : ) :
f.withBot =
theorem LatticeHom.withBot_apply {α : Type u_3} {β : Type u_4} [] [] (f : ) (a : ) :
f.withBot a = WithBot.map (⇑f) a
@[simp]
theorem LatticeHom.withBot_id {α : Type u_3} [] :
.withBot =
@[simp]
theorem LatticeHom.withBot_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [] [] [] (f : ) (g : ) :
(f.comp g).withBot = f.withBot.comp g.withBot
@[simp]
theorem LatticeHom.withTopWithBot_toLatticeHom {α : Type u_3} {β : Type u_4} [] [] (f : ) :
f.withTopWithBot.toLatticeHom = f.withBot.withTop
def LatticeHom.withTopWithBot {α : Type u_3} {β : Type u_4} [] [] (f : ) :

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.coe_withTopWithBot {α : Type u_3} {β : Type u_4} [] [] (f : ) :
f.withTopWithBot = Option.map (Option.map f)
theorem LatticeHom.withTopWithBot_apply {α : Type u_3} {β : Type u_4} [] [] (f : ) (a : WithTop (WithBot α)) :
f.withTopWithBot a = WithTop.map (Option.map f) a
@[simp]
theorem LatticeHom.withTopWithBot_id {α : Type u_3} [] :
.withTopWithBot =
@[simp]
theorem LatticeHom.withTopWithBot_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [] [] [] (f : ) (g : ) :
(f.comp g).withTopWithBot = f.withTopWithBot.comp g.withTopWithBot
@[simp]
theorem LatticeHom.withTop'_toSupHom {α : Type u_3} {β : Type u_4} [] [] [] (f : ) :
f.withTop'.toSupHom = f.withTop'
def LatticeHom.withTop' {α : Type u_3} {β : Type u_4} [] [] [] (f : ) :

Adjoins a ⊥ to the codomain of a LatticeHom.

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

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

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

Adjoins a ⊤ and ⊥ to the codomain of a LatticeHom.

Equations
• f.withTopWithBot' = { toLatticeHom := f.withBot'.withTop', map_top' := , map_bot' := }
Instances For