mathlib documentation

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 #

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) :
theorem antisymm_rel_refl {α : Type u_1} (r : α → α → Prop) [is_refl α r] (a : α) :
theorem antisymm_rel.symm {α : Type u_1} {r : α → α → Prop} {a b : α} :
antisymm_rel r a bantisymm_rel r b a
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 ba = 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] :
α → antisymmetrization α r

Turn an element into its antisymmetrization.

Equations
noncomputable def of_antisymmetrization {α : Type u_1} (r : α → α → Prop) [is_preorder α r] :
antisymmetrization α 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
@[simp]
theorem to_antisymmetrization_of_antisymmetrization {α : Type u_1} (r : α → α → Prop) [is_preorder α r] (a : antisymmetrization α r) :
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]
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 : antisymmetrization α has_le.le) :
@[simp]
theorem order_hom.antisymmetrization_apply_mk {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α →o β) (a : α) :