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 => { toFun := fun a => ↑f a ⊔ ↑g a, monotone' := (_ : Monotone (↑f ⊔ fun a => ↑g a)) } }

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

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

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

Equations

• OrderHom.instInfOrderHomToPreorderToPartialOrder = { inf := fun f g => { toFun := fun a => ↑f a ⊓ ↑g a, monotone' := (_ : Monotone (↑f ⊓ fun a => ↑g a)) } }

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

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

@[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 (_ : ∀ (x : α →o β) (x_1 : α), ⊥ ≤ OrderHom.toFun x x_1)

@[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 (_ : ∀ (x : α →o β) (x_1 : α), OrderHom.toFun x x_1 ≤ ⊤)

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

Equations

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

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

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

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

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

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₂