# Documentation

Mathlib.Order.Hom.Order

# 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 β→o β

## Tags #

monotone map, bundled morphism

instance OrderHom.instSupOrderHomToPreorderToPartialOrder {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] :
Sup (α →o β)
Equations
• OrderHom.instSupOrderHomToPreorderToPartialOrder = { sup := fun f g => { toFun := fun a => f a g a, monotone' := (_ : Monotone (f fun a => g a)) } }
@[simp]
theorem OrderHom.coe_sup {α : Type u_2} {β : Type u_1} [inst : ] [inst : ] (f : α →o β) (g : α →o β) :
↑(f g) = f g
instance OrderHom.instSemilatticeSupOrderHomToPreorderToPartialOrder {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] :
Equations
• One or more equations did not get rendered due to their size.
instance OrderHom.instInfOrderHomToPreorderToPartialOrder {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] :
Inf (α →o β)
Equations
• OrderHom.instInfOrderHomToPreorderToPartialOrder = { inf := fun f g => { toFun := fun a => f a g a, monotone' := (_ : Monotone (f fun a => g a)) } }
@[simp]
theorem OrderHom.coe_inf {α : Type u_2} {β : Type u_1} [inst : ] [inst : ] (f : α →o β) (g : α →o β) :
↑(f g) = f g
instance OrderHom.instSemilatticeInfOrderHomToPreorderToPartialOrder {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] :
Equations
• One or more equations did not get rendered due to their size.
instance OrderHom.lattice {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] :
Lattice (α →o β)
Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem OrderHom.instBotOrderHom_bot {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] [inst : ] :
= ↑()
instance OrderHom.instBotOrderHom {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] [inst : ] :
Bot (α →o β)
Equations
• OrderHom.instBotOrderHom = { bot := ↑() }
instance OrderHom.orderBot {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] [inst : ] :
OrderBot (α →o β)
Equations
@[simp]
theorem OrderHom.instTopOrderHom_top {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] [inst : ] :
= ↑()
instance OrderHom.instTopOrderHom {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] [inst : ] :
Top (α →o β)
Equations
• OrderHom.instTopOrderHom = { top := ↑() }
instance OrderHom.orderTop {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] [inst : ] :
OrderTop (α →o β)
Equations
instance OrderHom.instInfSetOrderHomToPreorderToPartialOrderToCompleteSemilatticeInf {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] :
InfSet (α →o β)
Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem OrderHom.infₛ_apply {α : Type u_2} {β : Type u_1} [inst : ] [inst : ] (s : Set (α →o β)) (x : α) :
↑(infₛ s) x = f, h, f x
theorem OrderHom.infᵢ_apply {α : Type u_3} {β : Type u_2} [inst : ] {ι : Sort u_1} [inst : ] (f : ια →o β) (x : α) :
↑(i, f i) x = i, ↑(f i) x
@[simp]
theorem OrderHom.coe_infᵢ {α : Type u_3} {β : Type u_2} [inst : ] {ι : Sort u_1} [inst : ] (f : ια →o β) :
↑(i, f i) = i, ↑(f i)
instance OrderHom.instSupSetOrderHomToPreorderToPartialOrderToCompleteSemilatticeInf {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] :
SupSet (α →o β)
Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem OrderHom.supₛ_apply {α : Type u_2} {β : Type u_1} [inst : ] [inst : ] (s : Set (α →o β)) (x : α) :
↑(supₛ s) x = f, h, f x
theorem OrderHom.supᵢ_apply {α : Type u_3} {β : Type u_2} [inst : ] {ι : Sort u_1} [inst : ] (f : ια →o β) (x : α) :
↑(i, f i) x = i, ↑(f i) x
@[simp]
theorem OrderHom.coe_supᵢ {α : Type u_3} {β : Type u_2} [inst : ] {ι : Sort u_1} [inst : ] (f : ια →o β) :
↑(i, f i) = i, ↑(f i)
Equations
• One or more equations did not get rendered due to their size.
theorem OrderHom.iterate_sup_le_sup_iff {α : Type u_1} [inst : ] (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₂