Category of preorders #
@[protected, instance]
def
preorder_hom.has_coe_to_fun
{α : Type u_1}
{β : Type u_2}
[preorder α]
[preorder β] :
has_coe_to_fun (α →ₘ β)
Equations
- preorder_hom.has_coe_to_fun = {F := λ (f : α →ₘ β), α → β, coe := preorder_hom.to_fun _inst_2}
The identity function as bundled monotone function.
@[simp]
@[protected, instance]
Equations
- preorder_hom.inhabited = {default := preorder_hom.id _inst_1}
@[simp]
@[simp]
theorem
preorder_hom.comp_id
{α : Type u_1}
{β : Type u_2}
[preorder α]
[preorder β]
(f : α →ₘ β) :
f.comp preorder_hom.id = f
@[simp]
theorem
preorder_hom.id_comp
{α : Type u_1}
{β : Type u_2}
[preorder α]
[preorder β]
(f : α →ₘ β) :
preorder_hom.id.comp f = f
subtype.val
as a bundled monotone function.
Equations
- preorder_hom.subtype.val p = {to_fun := subtype.val p, monotone' := _}
@[protected, instance]
The preorder structure of α →ₘ β
is pointwise inequality: f ≤ g ↔ ∀ a, f a ≤ g a
.
@[protected, instance]
def
preorder_hom.partial_order
{α : Type u_1}
[preorder α]
{β : Type u_2}
[partial_order β] :
partial_order (α →ₘ β)
Equations
- preorder_hom.partial_order = partial_order.lift preorder_hom.to_fun preorder_hom.partial_order._proof_1
@[protected, instance]
def
preorder_hom.semilattice_sup
{α : Type u_1}
[preorder α]
{β : Type u_2}
[semilattice_sup β] :
semilattice_sup (α →ₘ β)
Equations
- preorder_hom.semilattice_sup = {sup := has_sup.sup preorder_hom.has_sup, le := partial_order.le preorder_hom.partial_order, lt := partial_order.lt preorder_hom.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _}
@[protected, instance]
def
preorder_hom.semilattice_inf
{α : Type u_1}
[preorder α]
{β : Type u_2}
[semilattice_inf β] :
semilattice_inf (α →ₘ β)
Equations
- preorder_hom.semilattice_inf = {inf := has_inf.inf preorder_hom.has_inf, le := partial_order.le preorder_hom.partial_order, lt := partial_order.lt preorder_hom.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, inf_le_left := _, inf_le_right := _, le_inf := _}
@[protected, instance]
Equations
- preorder_hom.lattice = {sup := semilattice_sup.sup preorder_hom.semilattice_sup, le := semilattice_sup.le preorder_hom.semilattice_sup, lt := semilattice_sup.lt preorder_hom.semilattice_sup, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := semilattice_inf.inf preorder_hom.semilattice_inf, inf_le_left := _, inf_le_right := _, le_inf := _}
@[protected, instance]
Equations
- preorder_hom.order_bot = {bot := ⊥, le := partial_order.le preorder_hom.partial_order, lt := partial_order.lt preorder_hom.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, bot_le := _}
@[protected, instance]
Equations
- preorder_hom.order_top = {top := ⊤, le := partial_order.le preorder_hom.partial_order, lt := partial_order.lt preorder_hom.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_top := _}
@[simp]
theorem
preorder_hom.complete_lattice_Sup
{α : Type u_1}
[preorder α]
{β : Type u_2}
[complete_lattice β]
(ᾰ : set (α →ₘ β)) :
complete_lattice.Sup ᾰ = Sup ᾰ
@[simp]
theorem
preorder_hom.complete_lattice_Inf
{α : Type u_1}
[preorder α]
{β : Type u_2}
[complete_lattice β]
(ᾰ : set (α →ₘ β)) :
complete_lattice.Inf ᾰ = Inf ᾰ
@[protected, instance]
def
preorder_hom.complete_lattice
{α : Type u_1}
[preorder α]
{β : Type u_2}
[complete_lattice β] :
complete_lattice (α →ₘ β)
Equations
- preorder_hom.complete_lattice = {sup := lattice.sup preorder_hom.lattice, le := lattice.le preorder_hom.lattice, lt := lattice.lt preorder_hom.lattice, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := lattice.inf preorder_hom.lattice, inf_le_left := _, inf_le_right := _, le_inf := _, top := order_top.top preorder_hom.order_top, le_top := _, bot := order_bot.bot preorder_hom.order_bot, bot_le := _, Sup := Sup preorder_hom.has_Sup, le_Sup := _, Sup_le := _, Inf := Inf preorder_hom.has_Inf, Inf_le := _, le_Inf := _}
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
.
@[simp]
theorem
order_embedding.to_preorder_hom_coe
{X : Type u_1}
{Y : Type u_2}
[preorder X]
[preorder Y]
(f : X ↪o Y) :
⇑(f.to_preorder_hom) = ⇑f
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.
@[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) :
⇑(f.to_preorder_hom) = ⇑f
theorem
rel_embedding.to_preorder_hom_injective
{α : Type u_1}
{β : Type u_2}
[partial_order α]
[preorder β]
(f : has_lt.lt ↪r has_lt.lt) :