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.to_fun_eq_coe {α : 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) :
{to_fun := f, monotone' := hf} = f
@[ext]
theorem preorder_hom.ext {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f g : α →ₘ β) (h : f = g) :
f = g
def preorder_hom.id {α : Type u_1} [preorder α] :
α →ₘ α

The identity function as bundled monotone function.

Equations
@[simp]
theorem preorder_hom.id_coe {α : Type u_1} [preorder α] :
@[instance]
def preorder_hom.inhabited {α : Type u_1} [preorder α] :
Equations
@[simp]
theorem preorder_hom.comp_coe {α : Type u_1} {β : Type u_2} {γ : Type u_3} [preorder α] [preorder β] [preorder γ] (g : β →ₘ γ) (f : α →ₘ β) :
(g.comp f) = g f
def preorder_hom.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [preorder α] [preorder β] [preorder γ] (g : β →ₘ γ) (f : α →ₘ β) :
α →ₘ γ

The composition of two bundled monotone functions.

Equations
@[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
@[simp]
theorem preorder_hom.subtype.val_coe {α : Type u_1} [preorder α] (p : α → Prop) :
def preorder_hom.unique {α : Type u_1} [preorder α] [subsingleton α] :
unique →ₘ α)

There is a unique monotone map from a subsingleton to itself.

Equations
theorem preorder_hom.preorder_hom_eq_id {α : Type u_1} [preorder α] [subsingleton α] (g : α →ₘ α) :
@[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
@[instance]
def preorder_hom.has_sup {α : Type u_1} [preorder α] {β : Type u_2} [semilattice_sup β] :
has_sup →ₘ β)
Equations
@[simp]
theorem preorder_hom.has_sup_sup_coe {α : Type u_1} [preorder α] {β : Type u_2} [semilattice_sup β] (f g : α →ₘ β) (a : α) :
(f g) a = f a g a
@[simp]
theorem preorder_hom.has_inf_inf_coe {α : Type u_1} [preorder α] {β : Type u_2} [semilattice_inf β] (f g : α →ₘ β) (a : α) :
(f g) a = f a g a
@[instance]
def preorder_hom.has_inf {α : Type u_1} [preorder α] {β : Type u_2} [semilattice_inf β] :
has_inf →ₘ β)
Equations
@[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_coe {α : Type u_1} [preorder α] {β : Type u_2} [order_bot β] (a : α) :
@[simp]
theorem preorder_hom.has_top_top_coe {α : 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_coe {α : 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_coe {α : 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 β] (ᾰ : set →ₘ β)) :
@[simp]
theorem preorder_hom.complete_lattice_Inf {α : Type u_1} [preorder α] {β : Type u_2} [complete_lattice β] (ᾰ : set →ₘ β)) :
theorem preorder_hom.iterate_sup_le_sup_iff {α : Type u_1} [semilattice_sup α] (f : α →ₘ α) :
(∀ (n₁ n₂ : ) (a₁ a₂ : α), f^[n₁ + n₂] (a₁ a₂) f^[n₁] a₁ f^[n₂] a₂) ∀ (a₁ a₂ : α), f (a₁ a₂) f a₁ a₂
@[simp]
theorem order_embedding.to_preorder_hom_coe {X : Type u_1} {Y : Type u_2} [preorder X] [preorder Y] (f : X ↪o Y) :
def order_embedding.to_preorder_hom {X : Type u_1} {Y : Type u_2} [preorder X] [preorder Y] (f : X ↪o Y) :
X →ₘ Y

Convert an order_embedding to a preorder_hom.

Equations
@[simp]
theorem rel_hom.to_preorder_hom_coe {α : Type u_1} {β : Type u_2} [partial_order α] [preorder β] (f : has_lt.lt →r has_lt.lt) :
def rel_hom.to_preorder_hom {α : Type u_1} {β : Type u_2} [partial_order α] [preorder β] (f : has_lt.lt →r has_lt.lt) :
α →ₘ β

A bundled expression of the fact that a map between partial orders that is strictly monotonic is weakly monotonic.

Equations