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

@[protected, 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 : α →ₘ β) (h : ∀ (a : α), f a = g a) :
f = g
theorem preorder_hom.coe_inj {α : 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_to_fun {α : Type u_1} [preorder α] (a : α) :
@[protected, 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 γ] (g : β →ₘ γ) (f : α →ₘ β) :
α →ₘ γ

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 : α →ₘ β) (ᾰ : α) :
(g.comp f) = (g f)
@[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
@[protected, 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
@[protected, 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
@[protected, instance]
def preorder_hom.has_sup {α : Type u_1} [preorder α] {β : Type u_2} [semilattice_sup β] :
has_sup →ₘ β)
Equations
@[protected, 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
@[protected, 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 : α) :
@[protected, instance]
def preorder_hom.order_bot {α : Type u_1} [preorder α] {β : Type u_2} [order_bot β] :
Equations
@[simp]
theorem preorder_hom.has_top_top_to_fun {α : Type u_1} [preorder α] {β : Type u_2} [order_top β] (a : α) :
@[protected, instance]
def preorder_hom.has_top {α : Type u_1} [preorder α] {β : Type u_2} [order_top β] :
has_top →ₘ β)
Equations
@[protected, instance]
def preorder_hom.order_top {α : Type u_1} [preorder α] {β : Type u_2} [order_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)
@[protected, instance]
def preorder_hom.has_Inf {α : Type u_1} [preorder α] {β : Type u_2} [complete_lattice β] :
has_Inf →ₘ β)
Equations
@[protected, 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 β] (ᾰ : 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₂
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 order_embedding.to_preorder_hom_coe {X : Type u_1} {Y : Type u_2} [preorder X] [preorder Y] (f : X ↪o Y) :
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
@[simp]
theorem rel_hom.to_preorder_hom_coe_fn {α : Type u_1} {β : Type u_2} [partial_order α] [preorder β] (f : has_lt.lt →r has_lt.lt) :