mathlib3 documentation

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 #

def antisymm_rel {α : Type u_1} (r : α α Prop) (a b : α) :
Prop

The antisymmetrization relation.

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

Alias of the forward direction of antisymm_rel_iff_eq.

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

The antisymmetrization relation as an equivalence relation.

Equations
@[simp]
theorem antisymm_rel.setoid_r (α : Type u_1) (r : α α Prop) [is_preorder α r] (a b : α) :
a b = antisymm_rel r a b
def antisymmetrization (α : Type u_1) (r : α α Prop) [is_preorder α 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) [is_preorder α r] :

Turn an element into its antisymmetrization.

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

Get a representative from the antisymmetrization.

Equations
@[protected, instance]
def antisymmetrization.inhabited {α : Type u_1} (r : α α Prop) [is_preorder α r] [inhabited α] :
Equations
@[protected]
theorem antisymmetrization.ind {α : Type u_1} (r : α α Prop) [is_preorder α r] {p : antisymmetrization α r Prop} :
( (a : α), p (to_antisymmetrization r a)) (q : antisymmetrization α r), p q
@[protected]
theorem antisymmetrization.induction_on {α : Type u_1} (r : α α Prop) [is_preorder α r] {p : antisymmetrization α r Prop} (a : antisymmetrization α r) (h : (a : α), p (to_antisymmetrization r a)) :
p a
theorem antisymm_rel.image {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {a b : α} (h : antisymm_rel has_le.le a b) {f : α β} (hf : monotone f) :
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected]

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 : antisymmetrization α has_le.le) :