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 β)

Equations

• OrderHom.instSupOrderHomToPreorderToPartialOrder = { sup := fun (f g : α →o β) => { toFun := fun (a : α) => f a ⊔ g a, monotone' := ⋯ } }

@[simp]

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

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

Equations

• OrderHom.instSemilatticeSupOrderHomToPreorderToPartialOrder = let __src := OrderHom.instPartialOrderOrderHomToPreorder; SemilatticeSup.mk ⋯ ⋯ ⋯

instance OrderHom.instInfOrderHomToPreorderToPartialOrder {α : Type u_1} {β : Type u_2} [Preorder α] [SemilatticeInf β] : Inf (α →o β)

Equations

• OrderHom.instInfOrderHomToPreorderToPartialOrder = { inf := fun (f g : α →o β) => { toFun := fun (a : α) => f a ⊓ g a, monotone' := ⋯ } }

@[simp]

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

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• OrderHom.lattice = let __src := OrderHom.instSemilatticeSupOrderHomToPreorderToPartialOrder; let __src_1 := OrderHom.instSemilatticeInfOrderHomToPreorderToPartialOrder; Lattice.mk ⋯ ⋯ ⋯

@[simp]

theorem OrderHom.instBotOrderHom_bot {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [OrderBot β] : ⊥ = (OrderHom.const α) ⊥

instance OrderHom.instBotOrderHom {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [OrderBot β] : Bot (α →o β)

Equations

• OrderHom.instBotOrderHom = { bot := (OrderHom.const α) ⊥ }

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

Equations

• OrderHom.orderBot = OrderBot.mk ⋯

@[simp]

theorem OrderHom.instTopOrderHom_top {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [OrderTop β] : ⊤ = (OrderHom.const α) ⊤

instance OrderHom.instTopOrderHom {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [OrderTop β] : Top (α →o β)

Equations

• OrderHom.instTopOrderHom = { top := (OrderHom.const α) ⊤ }

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

Equations

• OrderHom.orderTop = OrderTop.mk ⋯

instance OrderHom.instInfSetOrderHomToPreorderToPartialOrderToCompleteSemilatticeInf {α : Type u_1} {β : Type u_2} [Preorder α] [CompleteLattice β] : InfSet (α →o β)

Equations

• OrderHom.instInfSetOrderHomToPreorderToPartialOrderToCompleteSemilatticeInf = { sInf := fun (s : Set (α →o β)) => { toFun := fun (x : α) => ⨅ f ∈ s, f x, monotone' := ⋯ } }

@[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)

instance OrderHom.instSupSetOrderHomToPreorderToPartialOrderToCompleteSemilatticeInf {α : Type u_1} {β : Type u_2} [Preorder α] [CompleteLattice β] : SupSet (α →o β)

Equations

• OrderHom.instSupSetOrderHomToPreorderToPartialOrderToCompleteSemilatticeInf = { sSup := fun (s : Set (α →o β)) => { toFun := fun (x : α) => ⨆ f ∈ s, f x, monotone' := ⋯ } }

@[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)

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

Equations

• One or more equations did not get rendered due to their size.

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₂