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.instSupOrderHomToPreorderToPartialOrder
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[SemilatticeSup β]
:
instance
OrderHom.instSemilatticeSupOrderHomToPreorderToPartialOrder
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[SemilatticeSup β]
:
SemilatticeSup (α →o β)
instance
OrderHom.instInfOrderHomToPreorderToPartialOrder
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[SemilatticeInf β]
:
instance
OrderHom.instSemilatticeInfOrderHomToPreorderToPartialOrder
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[SemilatticeInf β]
:
SemilatticeInf (α →o β)
instance
OrderHom.instInfSetOrderHomToPreorderToPartialOrderToCompleteSemilatticeInf
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[CompleteLattice β]
:
theorem
OrderHom.iInf_apply
{α : Type u_1}
{β : Type u_2}
[Preorder α]
{ι : Sort u_3}
[CompleteLattice β]
(f : ι → α →o β)
(x : α)
:
↑(⨅ (i : ι), f i) x = ⨅ (i : ι), ↑(f i) x
@[simp]
theorem
OrderHom.coe_iInf
{α : Type u_1}
{β : Type u_2}
[Preorder α]
{ι : Sort u_3}
[CompleteLattice β]
(f : ι → α →o β)
:
↑(⨅ (i : ι), f i) = ⨅ (i : ι), ↑(f i)
instance
OrderHom.instSupSetOrderHomToPreorderToPartialOrderToCompleteSemilatticeInf
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[CompleteLattice β]
:
theorem
OrderHom.iSup_apply
{α : Type u_1}
{β : Type u_2}
[Preorder α]
{ι : Sort u_3}
[CompleteLattice β]
(f : ι → α →o β)
(x : α)
:
↑(⨆ (i : ι), f i) x = ⨆ (i : ι), ↑(f i) x
@[simp]
theorem
OrderHom.coe_iSup
{α : Type u_1}
{β : Type u_2}
[Preorder α]
{ι : Sort u_3}
[CompleteLattice β]
(f : ι → α →o β)
:
↑(⨆ (i : ι), f i) = ⨆ (i : ι), ↑(f i)
instance
OrderHom.instCompleteLatticeOrderHomToPreorderToPartialOrderToCompleteSemilatticeInf
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[CompleteLattice β]
:
CompleteLattice (α →o β)