Documentation

Mathlib.Order.Hom.Order

Lattice structure on order homomorphisms #

This file defines the lattice structure on order homomorphisms, which are bundled monotone functions.

Main definitions #

Tags #

monotone map, bundled morphism

source
instance OrderHom.instSup {α : Type u_1} {β : Type u_2} [Preorder α] [SemilatticeSup β] :
Sup (α →o β)
Equations
  • OrderHom.instSup = { sup := fun (f g : α →o β) => { toFun := fun (a : α) => f a ⊔ g a, monotone' := ⋯ } }
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.instSemilatticeSup {α : Type u_1} {β : Type u_2} [Preorder α] [SemilatticeSup β] :
SemilatticeSup (α →o β)
Equations
source
instance OrderHom.instInf {α : Type u_1} {β : Type u_2} [Preorder α] [SemilatticeInf β] :
Inf (α →o β)
Equations
  • OrderHom.instInf = { inf := fun (f g : α →o β) => { toFun := fun (a : α) => f a ⊓ g a, monotone' := ⋯ } }
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.instSemilatticeInf {α : Type u_1} {β : Type u_2} [Preorder α] [SemilatticeInf β] :
SemilatticeInf (α →o β)
Equations
source
instance OrderHom.lattice {α : Type u_1} {β : Type u_2} [Preorder α] [Lattice β] :
Lattice (α →o β)
Equations
source
instance OrderHom.instBotOfOrderBot {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [OrderBot β] :
Bot (α →o β)
Equations
source
@[simp]
theorem OrderHom.instBotOfOrderBot_bot {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [OrderBot β] :
⊥ = (OrderHom.const α) ⊥
source
instance OrderHom.orderBot {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [OrderBot β] :
OrderBot (α →o β)
Equations
source
instance OrderHom.instTopOrderHom {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [OrderTop β] :
Top (α →o β)
Equations
source
@[simp]
theorem OrderHom.instTopOrderHom_top {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [OrderTop β] :
⊤ = (OrderHom.const α) ⊤
source
instance OrderHom.orderTop {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [OrderTop β] :
OrderTop (α →o β)
Equations
source
instance OrderHom.instInfSet {α : Type u_1} {β : Type u_2} [Preorder α] [CompleteLattice β] :
InfSet (α →o β)
Equations
  • OrderHom.instInfSet = { sInf := fun (s : Set (α →o β)) => { toFun := fun (x : α) => ⨅ f ∈ s, f x, monotone' := ⋯ } }
source
@[simp]
theorem OrderHom.sInf_apply {α : Type u_1} {β : Type u_2} [Preorder α] [CompleteLattice β] (s : Set (α →o β)) (x : α) :
(sInf s) x = ⨅ 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.instSupSet {α : Type u_1} {β : Type u_2} [Preorder α] [CompleteLattice β] :
SupSet (α →o β)
Equations
  • OrderHom.instSupSet = { sSup := fun (s : Set (α →o β)) => { toFun := fun (x : α) => ⨆ f ∈ s, f x, monotone' := ⋯ } }
source
@[simp]
theorem OrderHom.sSup_apply {α : Type u_1} {β : Type u_2} [Preorder α] [CompleteLattice β] (s : Set (α →o β)) (x : α) :
(sSup s) x = ⨆ 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.instCompleteLattice {α : Type u_1} {β : Type u_2} [Preorder α] [CompleteLattice β] :
CompleteLattice (α →o β)
Equations
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₂