# mathlib3documentation

order.antisymmetrization

# Turning a preorder into a partial order #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file allows to make a preorder into a partial order by quotienting out the elements a, b such that a ≤ b and b ≤ a.

antisymmetrization is a functor from Preorder to PartialOrder. See Preorder_to_PartialOrder.

## Main declarations #

• antisymm_rel: The antisymmetrization relation. antisymm_rel r a b means that a and b are related both ways by r.
• antisymmetrization α r: The quotient of α by antisymm_rel r. Even when r is just a preorder, antisymmetrization α is a partial order.
def antisymm_rel {α : Type u_1} (r : α α Prop) (a b : α) :
Prop

The antisymmetrization relation.

Equations
• a b = (r a b r b a)
Instances for antisymm_rel
theorem antisymm_rel_swap {α : Type u_1} (r : α α Prop) :
@[refl]
theorem antisymm_rel_refl {α : Type u_1} (r : α α Prop) [ r] (a : α) :
a a
@[symm]
theorem antisymm_rel.symm {α : Type u_1} {r : α α Prop} {a b : α} :
a b b a
@[trans]
theorem antisymm_rel.trans {α : Type u_1} {r : α α Prop} [ r] {a b c : α} (hab : a b) (hbc : b c) :
a c
@[protected, instance]
def antisymm_rel.decidable_rel {α : Type u_1} {r : α α Prop}  :
Equations
@[simp]
theorem antisymm_rel_iff_eq {α : Type u_1} {r : α α Prop} [ r] [ r] {a b : α} :
a b a = b
theorem antisymm_rel.eq {α : Type u_1} {r : α α Prop} [ r] [ r] {a b : α} :
a b a = b

Alias of the forward direction of antisymm_rel_iff_eq.

def antisymm_rel.setoid (α : Type u_1) (r : α α Prop) [ r] :

The antisymmetrization relation as an equivalence relation.

Equations
@[simp]
theorem antisymm_rel.setoid_r (α : Type u_1) (r : α α Prop) [ r] (a b : α) :
a b = a b
def antisymmetrization (α : Type u_1) (r : α α Prop) [ r] :
Type u_1

The partial order derived from a preorder by making pairwise comparable elements equal. This is the quotient by λ a b, a ≤ b ∧ b ≤ a.

Equations
Instances for antisymmetrization
def to_antisymmetrization {α : Type u_1} (r : α α Prop) [ r] :
α

Turn an element into its antisymmetrization.

Equations
noncomputable def of_antisymmetrization {α : Type u_1} (r : α α Prop) [ r] :
α

Get a representative from the antisymmetrization.

Equations
@[protected, instance]
def antisymmetrization.inhabited {α : Type u_1} (r : α α Prop) [ r] [inhabited α] :
Equations
@[protected]
theorem antisymmetrization.ind {α : Type u_1} (r : α α Prop) [ r] {p : Prop} :
( (a : α), p a)) (q : , p q
@[protected]
theorem antisymmetrization.induction_on {α : Type u_1} (r : α α Prop) [ r] {p : Prop} (a : r) (h : (a : α), p ) :
p a
@[simp]
theorem to_antisymmetrization_of_antisymmetrization {α : Type u_1} (r : α α Prop) [ r] (a : r) :
theorem antisymm_rel.image {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {a b : α} (h : b) {f : α β} (hf : monotone f) :
(f a) (f b)
@[protected, instance]
Equations
theorem antisymmetrization_fibration {α : Type u_1} [preorder α] :
theorem acc_antisymmetrization_iff {α : Type u_1} [preorder α] {a : α} :
@[protected, instance]
@[protected, instance]
Equations
@[simp]
theorem to_antisymmetrization_le_to_antisymmetrization_iff {α : Type u_1} [preorder α] {a b : α} :
@[simp]
theorem to_antisymmetrization_lt_to_antisymmetrization_iff {α : Type u_1} [preorder α] {a b : α} :
theorem to_antisymmetrization_mono {α : Type u_1} [preorder α] :

to_antisymmetrization as an order homomorphism.

Equations
@[simp]
theorem order_hom.to_antisymmetrization_coe {α : Type u_1} [preorder α] (ᾰ : α) :
@[protected]
def order_hom.antisymmetrization {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α →o β) :

Turns an order homomorphism from α to β into one from antisymmetrization α to antisymmetrization β. antisymmetrization is actually a functor. See Preorder_to_PartialOrder.

Equations
@[simp]
theorem order_hom.coe_antisymmetrization {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α →o β) :
@[simp]
theorem order_hom.antisymmetrization_apply {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α →o β) (a : has_le.le) :
@[simp]
theorem order_hom.antisymmetrization_apply_mk {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α →o β) (a : α) :
noncomputable def order_embedding.of_antisymmetrization (α : Type u_1) [preorder α] :

of_antisymmetrization as an order embedding.

Equations
@[simp]

antisymmetrization and order_dual commute.

Equations
@[simp]
theorem order_iso.dual_antisymmetrization_apply (α : Type u_1) [preorder α] (a : α) :
@[simp]
theorem order_iso.dual_antisymmetrization_symm_apply (α : Type u_1) [preorder α] (a : α) :