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

instance OrderHom.instSupOrderHomToPreorderToPartialOrder {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : 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_2} {β : Type u_1} [inst : Preorder α] [inst : SemilatticeSup β] (f : α →o β) (g : α →o β) :
↑(f g) = f g
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 β] :
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_2} {β : Type u_1} [inst : Preorder α] [inst : SemilatticeInf β] (f : α →o β) (g : α →o β) :
↑(f g) = f g
Equations
  • One or more equations did not get rendered due to their size.
instance OrderHom.lattice {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : 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} [inst : Preorder α] [inst : Preorder β] [inst : OrderBot β] :
instance OrderHom.instBotOrderHom {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : OrderBot β] :
Bot (α →o β)
Equations
instance OrderHom.orderBot {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : OrderBot β] :
OrderBot (α →o β)
Equations
@[simp]
theorem OrderHom.instTopOrderHom_top {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : OrderTop β] :
instance OrderHom.instTopOrderHom {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : OrderTop β] :
Top (α →o β)
Equations
instance OrderHom.orderTop {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : OrderTop β] :
OrderTop (α →o β)
Equations
Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem OrderHom.infₛ_apply {α : Type u_2} {β : Type u_1} [inst : Preorder α] [inst : CompleteLattice β] (s : Set (α →o β)) (x : α) :
↑(infₛ s) x = f, h, f x
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)
Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem OrderHom.supₛ_apply {α : Type u_2} {β : Type u_1} [inst : Preorder α] [inst : CompleteLattice β] (s : Set (α →o β)) (x : α) :
↑(supₛ s) x = f, h, f x
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)
Equations
  • One or more equations did not get rendered due to their size.
theorem OrderHom.iterate_sup_le_sup_iff {α : Type u_1} [inst : 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₂