mathlib documentation

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

@[protected, instance]
def order_hom.has_sup {α : Type u_1} {β : Type u_2} [preorder α] [semilattice_sup β] :
has_sup →o β)
Equations
@[simp]
theorem order_hom.has_sup_sup_coe {α : Type u_1} {β : Type u_2} [preorder α] [semilattice_sup β] (f g : α →o β) (a : α) :
(f g) a = f a g a
@[simp]
theorem order_hom.has_inf_inf_coe {α : Type u_1} {β : Type u_2} [preorder α] [semilattice_inf β] (f g : α →o β) (a : α) :
(f g) a = f a g a
@[protected, instance]
def order_hom.has_inf {α : Type u_1} {β : Type u_2} [preorder α] [semilattice_inf β] :
has_inf →o β)
Equations
@[protected, instance]
def order_hom.has_bot {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] [order_bot β] :
has_bot →o β)
Equations
@[simp]
theorem order_hom.has_bot_bot {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] [order_bot β] :
@[protected, instance]
def order_hom.order_bot {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] [order_bot β] :
order_bot →o β)
Equations
@[simp]
theorem order_hom.has_top_top {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] [order_top β] :
@[protected, instance]
def order_hom.has_top {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] [order_top β] :
has_top →o β)
Equations
@[protected, instance]
def order_hom.order_top {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] [order_top β] :
order_top →o β)
Equations
@[protected, instance]
def order_hom.has_Inf {α : Type u_1} {β : Type u_2} [preorder α] [complete_lattice β] :
has_Inf →o β)
Equations
@[simp]
theorem order_hom.Inf_apply {α : Type u_1} {β : Type u_2} [preorder α] [complete_lattice β] (s : set →o β)) (x : α) :
(has_Inf.Inf s) x = ⨅ (f : α →o β) (H : f s), f x
theorem order_hom.infi_apply {α : Type u_1} {β : Type u_2} [preorder α] {ι : Sort u_3} [complete_lattice β] (f : ι → α →o β) (x : α) :
(⨅ (i : ι), f i) x = ⨅ (i : ι), (f i) x
@[simp, norm_cast]
theorem order_hom.coe_infi {α : Type u_1} {β : Type u_2} [preorder α] {ι : Sort u_3} [complete_lattice β] (f : ι → α →o β) :
(⨅ (i : ι), f i) = ⨅ (i : ι), (f i)
@[protected, instance]
def order_hom.has_Sup {α : Type u_1} {β : Type u_2} [preorder α] [complete_lattice β] :
has_Sup →o β)
Equations
@[simp]
theorem order_hom.Sup_apply {α : Type u_1} {β : Type u_2} [preorder α] [complete_lattice β] (s : set →o β)) (x : α) :
(has_Sup.Sup s) x = ⨆ (f : α →o β) (H : f s), f x
theorem order_hom.supr_apply {α : Type u_1} {β : Type u_2} [preorder α] {ι : Sort u_3} [complete_lattice β] (f : ι → α →o β) (x : α) :
(⨆ (i : ι), f i) x = ⨆ (i : ι), (f i) x
@[simp, norm_cast]
theorem order_hom.coe_supr {α : Type u_1} {β : Type u_2} [preorder α] {ι : Sort u_3} [complete_lattice β] (f : ι → α →o β) :
(⨆ (i : ι), f i) = ⨆ (i : ι), (f i)
theorem order_hom.iterate_sup_le_sup_iff {α : Type u_1} [semilattice_sup α] (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₂