Lattice structure on order homomorphisms #
This file defines the lattice structure on order homomorphisms, which are bundled monotone functions.
Main definitions #
OrderHom.instCompleteLattice: ifβis a complete lattice, so isα →o β
Tags #
monotone map, bundled morphism
@[implicit_reducible]
instance
OrderHom.instMax
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[SemilatticeSup β]
:
Max (α →o β)
@[simp]
theorem
OrderHom.coe_sup
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[SemilatticeSup β]
(f g : α →o β)
:
⇑(f ⊔ g) = ⇑f ⊔ ⇑g
@[implicit_reducible]
instance
OrderHom.instSemilatticeSup
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[SemilatticeSup β]
:
SemilatticeSup (α →o β)
@[implicit_reducible]
instance
OrderHom.instMin
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[SemilatticeInf β]
:
Min (α →o β)
@[simp]
theorem
OrderHom.coe_inf
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[SemilatticeInf β]
(f g : α →o β)
:
⇑(f ⊓ g) = ⇑f ⊓ ⇑g
@[implicit_reducible]
instance
OrderHom.instSemilatticeInf
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[SemilatticeInf β]
:
SemilatticeInf (α →o β)
@[implicit_reducible]
@[implicit_reducible]
@[implicit_reducible]
@[implicit_reducible]
@[implicit_reducible]
@[implicit_reducible]
@[simp]
theorem
OrderHom.sInf_apply
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[CompleteLattice β]
(s : Set (α →o β))
(x : α)
:
(sInf s) x = ⨅ f ∈ s, f x
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)
@[implicit_reducible]
@[simp]
theorem
OrderHom.sSup_apply
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[CompleteLattice β]
(s : Set (α →o β))
(x : α)
:
(sSup s) x = ⨆ f ∈ s, f x
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)
@[implicit_reducible]
instance
OrderHom.instCompleteLattice
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[CompleteLattice β]
:
CompleteLattice (α →o β)