# Lattice structure on order homomorphisms #

This file defines the lattice structure on order homomorphisms, which are bundled monotone functions.

## Main definitions #

• OrderHom.CompleteLattice: if β is a complete lattice, so is α →o β

## Tags #

monotone map, bundled morphism

instance OrderHom.instSup {α : Type u_1} {β : Type u_2} [] [] :
Sup (α →o β)
Equations
• OrderHom.instSup = { sup := fun (f g : α →o β) => { toFun := fun (a : α) => f a g a, monotone' := } }
@[simp]
theorem OrderHom.coe_sup {α : Type u_1} {β : Type u_2} [] [] (f : α →o β) (g : α →o β) :
(f g) = f g
instance OrderHom.instSemilatticeSup {α : Type u_1} {β : Type u_2} [] [] :
Equations
• OrderHom.instSemilatticeSup = let __src := OrderHom.instPartialOrder;
instance OrderHom.instInf {α : Type u_1} {β : Type u_2} [] [] :
Inf (α →o β)
Equations
• OrderHom.instInf = { inf := fun (f g : α →o β) => { toFun := fun (a : α) => f a g a, monotone' := } }
@[simp]
theorem OrderHom.coe_inf {α : Type u_1} {β : Type u_2} [] [] (f : α →o β) (g : α →o β) :
(f g) = f g
instance OrderHom.instSemilatticeInf {α : Type u_1} {β : Type u_2} [] [] :
Equations
• OrderHom.instSemilatticeInf = let __src := OrderHom.instPartialOrder; let __src_1 := (OrderHom.dualIso α β).symm.toGaloisInsertion.liftSemilatticeInf;
instance OrderHom.lattice {α : Type u_1} {β : Type u_2} [] [] :
Lattice (α →o β)
Equations
• OrderHom.lattice = let __src := OrderHom.instSemilatticeSup; let __src_1 := OrderHom.instSemilatticeInf; Lattice.mk
@[simp]
theorem OrderHom.instBotOfOrderBot_bot {α : Type u_1} {β : Type u_2} [] [] [] :
instance OrderHom.instBotOfOrderBot {α : Type u_1} {β : Type u_2} [] [] [] :
Bot (α →o β)
Equations
• OrderHom.instBotOfOrderBot = { bot := }
instance OrderHom.orderBot {α : Type u_1} {β : Type u_2} [] [] [] :
OrderBot (α →o β)
Equations
• OrderHom.orderBot =
@[simp]
theorem OrderHom.instTopOrderHom_top {α : Type u_1} {β : Type u_2} [] [] [] :
instance OrderHom.instTopOrderHom {α : Type u_1} {β : Type u_2} [] [] [] :
Top (α →o β)
Equations
• OrderHom.instTopOrderHom = { top := }
instance OrderHom.orderTop {α : Type u_1} {β : Type u_2} [] [] [] :
OrderTop (α →o β)
Equations
• OrderHom.orderTop =
instance OrderHom.instInfSet {α : Type u_1} {β : Type u_2} [] [] :
InfSet (α →o β)
Equations
• OrderHom.instInfSet = { sInf := fun (s : Set (α →o β)) => { toFun := fun (x : α) => fs, f x, monotone' := } }
@[simp]
theorem OrderHom.sInf_apply {α : Type u_1} {β : Type u_2} [] [] (s : Set (α →o β)) (x : α) :
(sInf s) x = fs, f x
theorem OrderHom.iInf_apply {α : Type u_1} {β : Type u_2} [] {ι : Sort u_3} [] (f : ια →o β) (x : α) :
(⨅ (i : ι), f i) x = ⨅ (i : ι), (f i) x
@[simp]
theorem OrderHom.coe_iInf {α : Type u_1} {β : Type u_2} [] {ι : Sort u_3} [] (f : ια →o β) :
(⨅ (i : ι), f i) = ⨅ (i : ι), (f i)
instance OrderHom.instSupSet {α : Type u_1} {β : Type u_2} [] [] :
SupSet (α →o β)
Equations
• OrderHom.instSupSet = { sSup := fun (s : Set (α →o β)) => { toFun := fun (x : α) => fs, f x, monotone' := } }
@[simp]
theorem OrderHom.sSup_apply {α : Type u_1} {β : Type u_2} [] [] (s : Set (α →o β)) (x : α) :
(sSup s) x = fs, f x
theorem OrderHom.iSup_apply {α : Type u_1} {β : Type u_2} [] {ι : Sort u_3} [] (f : ια →o β) (x : α) :
(⨆ (i : ι), f i) x = ⨆ (i : ι), (f i) x
@[simp]
theorem OrderHom.coe_iSup {α : Type u_1} {β : Type u_2} [] {ι : Sort u_3} [] (f : ια →o β) :
(⨆ (i : ι), f i) = ⨆ (i : ι), (f i)
instance OrderHom.instCompleteLattice {α : Type u_1} {β : Type u_2} [] [] :
Equations
• OrderHom.instCompleteLattice = let __src := OrderHom.lattice; let __src_1 := OrderHom.orderTop; let __src_2 := OrderHom.orderBot; CompleteLattice.mk
theorem OrderHom.iterate_sup_le_sup_iff {α : Type u_3} [] (f : α →o α) :
(∀ (n₁ n₂ : ) (a₁ a₂ : α), (⇑f)^[n₁ + n₂] (a₁ a₂) (⇑f)^[n₁] a₁ (⇑f)^[n₂] a₂) ∀ (a₁ a₂ : α), f (a₁ a₂) f a₁ a₂