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 : Preorder α]
[inst : SemilatticeSup β]
:
instance
OrderHom.instSemilatticeSupOrderHomToPreorderToPartialOrder
{α : Type u_1}
{β : Type u_2}
[inst : Preorder α]
[inst : SemilatticeSup β]
:
SemilatticeSup (α →o β)
Equations
- One or more equations did not get rendered due to their size.
instance
OrderHom.instInfOrderHomToPreorderToPartialOrder
{α : Type u_1}
{β : Type u_2}
[inst : Preorder α]
[inst : SemilatticeInf β]
:
instance
OrderHom.instSemilatticeInfOrderHomToPreorderToPartialOrder
{α : Type u_1}
{β : Type u_2}
[inst : Preorder α]
[inst : SemilatticeInf β]
:
SemilatticeInf (α →o β)
Equations
- One or more equations did not get rendered due to their size.
instance
OrderHom.instInfSetOrderHomToPreorderToPartialOrderToCompleteSemilatticeInf
{α : Type u_1}
{β : Type u_2}
[inst : Preorder α]
[inst : CompleteLattice β]
:
Equations
- One or more equations did not get rendered due to their size.
theorem
OrderHom.infᵢ_apply
{α : Type u_3}
{β : Type u_2}
[inst : Preorder α]
{ι : Sort u_1}
[inst : CompleteLattice β]
(f : ι → α →o β)
(x : α)
:
↑(⨅ i, f i) x = ⨅ i, ↑(f i) x
@[simp]
theorem
OrderHom.coe_infᵢ
{α : Type u_3}
{β : Type u_2}
[inst : Preorder α]
{ι : Sort u_1}
[inst : CompleteLattice β]
(f : ι → α →o β)
:
↑(⨅ i, f i) = ⨅ i, ↑(f i)
instance
OrderHom.instSupSetOrderHomToPreorderToPartialOrderToCompleteSemilatticeInf
{α : Type u_1}
{β : Type u_2}
[inst : Preorder α]
[inst : CompleteLattice β]
:
Equations
- One or more equations did not get rendered due to their size.
theorem
OrderHom.supᵢ_apply
{α : Type u_3}
{β : Type u_2}
[inst : Preorder α]
{ι : Sort u_1}
[inst : CompleteLattice β]
(f : ι → α →o β)
(x : α)
:
↑(⨆ i, f i) x = ⨆ i, ↑(f i) x
@[simp]
theorem
OrderHom.coe_supᵢ
{α : Type u_3}
{β : Type u_2}
[inst : Preorder α]
{ι : Sort u_1}
[inst : CompleteLattice β]
(f : ι → α →o β)
:
↑(⨆ i, f i) = ⨆ i, ↑(f i)
instance
OrderHom.instCompleteLatticeOrderHomToPreorderToPartialOrderToCompleteSemilatticeInf
{α : Type u_1}
{β : Type u_2}
[inst : Preorder α]
[inst : CompleteLattice β]
:
CompleteLattice (α →o β)
Equations
- One or more equations did not get rendered due to their size.