mathlib documentation

order.preorder_hom

Category of preorders

structure preorder_hom (α : Type u_1) (β : Type u_2) [preorder α] [preorder β] :
Type (max u_1 u_2)

Bundled monotone (aka, increasing) function

@[instance]
def preorder_hom.has_coe_to_fun {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] :

Equations
theorem preorder_hom.monotone {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α →ₘ β) :

@[simp]
theorem preorder_hom.coe_fun_mk {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {f : α → β} (hf : monotone f) (x : α) :
{to_fun := f, monotone' := hf} x = f x

@[ext]
theorem preorder_hom.ext {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f g : α →ₘ β) :
(∀ (a : α), f a = g a)f = g

theorem preorder_hom.coe_inj {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f g : α →ₘ β) :
f = gf = g

def preorder_hom.id {α : Type u_1} [preorder α] :
α →ₘ α

The identity function as bundled monotone function.

Equations
@[simp]
theorem preorder_hom.id_to_fun {α : Type u_1} [preorder α] (a : α) :

@[instance]
def preorder_hom.inhabited {α : Type u_1} [preorder α] :

Equations
@[simp]

def preorder_hom.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [preorder α] [preorder β] [preorder γ] :
→ₘ γ)→ₘ β)α →ₘ γ

The composition of two bundled monotone functions.

Equations
@[simp]
theorem preorder_hom.comp_to_fun {α : Type u_1} {β : Type u_2} {γ : Type u_3} [preorder α] [preorder β] [preorder γ] (g : β →ₘ γ) (f : α →ₘ β) (a : α) :
(g.comp f) a = (g f) a

@[simp]
theorem preorder_hom.comp_id {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α →ₘ β) :

@[simp]
theorem preorder_hom.id_comp {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α →ₘ β) :

def preorder_hom.subtype.val {α : Type u_1} [preorder α] (p : α → Prop) :

subtype.val as a bundled monotone function.

Equations
@[instance]
def preorder_hom.preorder {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] :

The preorder structure of α →ₘ β is pointwise inequality: f ≤ g ↔ ∀ a, f a ≤ g a.

Equations
@[instance]
def preorder_hom.partial_order {α : Type u_1} [preorder α] {β : Type u_2} [partial_order β] :

Equations
@[simp]
theorem preorder_hom.has_sup_sup_to_fun {α : Type u_1} [preorder α] {β : Type u_2} [semilattice_sup β] (f g : α →ₘ β) (a : α) :
(f g) a = f a g a

@[instance]
def preorder_hom.has_sup {α : Type u_1} [preorder α] {β : Type u_2} [semilattice_sup β] :
has_sup →ₘ β)

Equations
@[instance]
def preorder_hom.has_inf {α : Type u_1} [preorder α] {β : Type u_2} [semilattice_inf β] :
has_inf →ₘ β)

Equations
@[simp]
theorem preorder_hom.has_inf_inf_to_fun {α : Type u_1} [preorder α] {β : Type u_2} [semilattice_inf β] (f g : α →ₘ β) (a : α) :
(f g) a = f a g a

@[instance]
def preorder_hom.has_bot {α : Type u_1} [preorder α] {β : Type u_2} [order_bot β] :
has_bot →ₘ β)

Equations
@[simp]
theorem preorder_hom.has_bot_bot_to_fun {α : Type u_1} [preorder α] {β : Type u_2} [order_bot β] (a : α) :

@[simp]
theorem preorder_hom.has_top_top_to_fun {α : Type u_1} [preorder α] {β : Type u_2} [order_top β] (a : α) :

@[instance]
def preorder_hom.has_top {α : Type u_1} [preorder α] {β : Type u_2} [order_top β] :
has_top →ₘ β)

Equations
@[simp]
theorem preorder_hom.has_Inf_Inf_to_fun {α : Type u_1} [preorder α] {β : Type u_2} [complete_lattice β] (s : set →ₘ β)) (x : α) :
(Inf s) x = Inf ((λ (f : α →ₘ β), f x) '' s)

@[instance]
def preorder_hom.has_Inf {α : Type u_1} [preorder α] {β : Type u_2} [complete_lattice β] :
has_Inf →ₘ β)

Equations
@[instance]
def preorder_hom.has_Sup {α : Type u_1} [preorder α] {β : Type u_2} [complete_lattice β] :
has_Sup →ₘ β)

Equations
@[simp]
theorem preorder_hom.has_Sup_Sup_to_fun {α : Type u_1} [preorder α] {β : Type u_2} [complete_lattice β] (s : set →ₘ β)) (x : α) :
(Sup s) x = Sup ((λ (f : α →ₘ β), f x) '' s)

@[simp]
theorem preorder_hom.complete_lattice_Sup {α : Type u_1} [preorder α] {β : Type u_2} [complete_lattice β] (a : set →ₘ β)) :

@[simp]
theorem preorder_hom.complete_lattice_Inf {α : Type u_1} [preorder α] {β : Type u_2} [complete_lattice β] (a : set →ₘ β)) :