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 β] :

Sup (α →o β)

source

@[simp]

theorem OrderHom.coe_sup {α : Type u_1} {β : Type u_2} [Preorder α] [SemilatticeSup β] (f : α →o β) (g : α →o β) :

↑(f ⊔ g) = ↑f ⊔ ↑g

source

instance OrderHom.instSemilatticeSupOrderHomToPreorderToPartialOrder {α : Type u_1} {β : Type u_2} [Preorder α] [SemilatticeSup β] :

SemilatticeSup (α →o β)

source

instance OrderHom.instInfOrderHomToPreorderToPartialOrder {α : Type u_1} {β : Type u_2} [Preorder α] [SemilatticeInf β] :

Inf (α →o β)

source

@[simp]

theorem OrderHom.coe_inf {α : Type u_1} {β : Type u_2} [Preorder α] [SemilatticeInf β] (f : α →o β) (g : α →o β) :

↑(f ⊓ g) = ↑f ⊓ ↑g

source

instance OrderHom.instSemilatticeInfOrderHomToPreorderToPartialOrder {α : Type u_1} {β : Type u_2} [Preorder α] [SemilatticeInf β] :

SemilatticeInf (α →o β)

source

instance OrderHom.lattice {α : Type u_1} {β : Type u_2} [Preorder α] [Lattice β] :

Lattice (α →o β)

source

@[simp]

theorem OrderHom.instBotOrderHom_bot {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [OrderBot β] :

⊥ = ↑(OrderHom.const α) ⊥

source

instance OrderHom.instBotOrderHom {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [OrderBot β] :

Bot (α →o β)

source

instance OrderHom.orderBot {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [OrderBot β] :

OrderBot (α →o β)

source

@[simp]

theorem OrderHom.instTopOrderHom_top {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [OrderTop β] :

⊤ = ↑(OrderHom.const α) ⊤

source

instance OrderHom.instTopOrderHom {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [OrderTop β] :

Top (α →o β)

source

instance OrderHom.orderTop {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [OrderTop β] :

OrderTop (α →o β)

source

instance OrderHom.instInfSetOrderHomToPreorderToPartialOrderToCompleteSemilatticeInf {α : Type u_1} {β : Type u_2} [Preorder α] [CompleteLattice β] :

InfSet (α →o β)

source

@[simp]

theorem OrderHom.sInf_apply {α : Type u_1} {β : Type u_2} [Preorder α] [CompleteLattice β] (s : Set (α →o β)) (x : α) :

↑(sInf s) x = ⨅ (f : α →o β) (_ : f ∈ s), ↑f x

source

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

source

@[simp]

theorem OrderHom.coe_iInf {α : Type u_1} {β : Type u_2} [Preorder α] {ι : Sort u_3} [CompleteLattice β] (f : ι → α →o β) :

↑(⨅ (i : ι), f i) = ⨅ (i : ι), ↑(f i)

source

instance OrderHom.instSupSetOrderHomToPreorderToPartialOrderToCompleteSemilatticeInf {α : Type u_1} {β : Type u_2} [Preorder α] [CompleteLattice β] :

SupSet (α →o β)

source

@[simp]

theorem OrderHom.sSup_apply {α : Type u_1} {β : Type u_2} [Preorder α] [CompleteLattice β] (s : Set (α →o β)) (x : α) :

↑(sSup s) x = ⨆ (f : α →o β) (_ : f ∈ s), ↑f x

source

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

source

@[simp]

theorem OrderHom.coe_iSup {α : Type u_1} {β : Type u_2} [Preorder α] {ι : Sort u_3} [CompleteLattice β] (f : ι → α →o β) :

↑(⨆ (i : ι), f i) = ⨆ (i : ι), ↑(f i)

source

instance OrderHom.instCompleteLatticeOrderHomToPreorderToPartialOrderToCompleteSemilatticeInf {α : Type u_1} {β : Type u_2} [Preorder α] [CompleteLattice β] :

CompleteLattice (α →o β)

source

theorem OrderHom.iterate_sup_le_sup_iff {α : Type u_3} [SemilatticeSup α] (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₂