# mathlibdocumentation

order.antisymmetrization

# Turning a preorder into a partial order #

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 ba = 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]
def antisymmetrization.partial_order {α : Type u_1} [preorder α] :
Equations
@[protected, instance]
def antisymmetrization.linear_order {α : Type u_1} [preorder α]  :
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 : α} :
@[simp]
@[simp]
theorem to_antisymmetrization_mono {α : Type u_1} [preorder α] :
def order_hom.to_antisymmetrization {α : 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]
theorem order_embedding.of_antisymmetrization_apply (α : Type u_1) [preorder α] (ᾰ : has_le.le) :
def order_iso.dual_antisymmetrization (α : Type u_1) [preorder α] :

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 : α) :