Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-16 17:16 6bcb12c1

View on Github →

feat(order/antisymmetrization): Turning a preorder into a partial order (#11728) Define antisymmetrization, the quotient of a preorder by the "less than both ways" relation. This effectively turns a preorder into a partial order, and this operation is functorial as shown by the new Preorder_to_PartialOrder.

Estimated changes

Modified src/data/quot.lean

Created src/order/antisymmetrization.lean

added theorem antisymm_rel.image

added def antisymm_rel.setoid

added theorem antisymm_rel.symm

added theorem antisymm_rel.trans

added def antisymm_rel

added theorem antisymm_rel_iff_eq

added theorem antisymm_rel_refl

added theorem antisymm_rel_swap

added def antisymmetrization

added theorem of_antisymmetrization_le_of_antisymmetrization_iff

added theorem of_antisymmetrization_lt_of_antisymmetrization_iff

added theorem order_hom.antisymmetrization_apply

added theorem order_hom.antisymmetrization_apply_mk

added theorem order_hom.coe_antisymmetrization

added def order_hom.to_antisymmetrization

added def order_iso.dual_antisymmetrization

added theorem order_iso.dual_antisymmetrization_apply

added theorem order_iso.dual_antisymmetrization_symm_apply

added def to_antisymmetrization

added theorem to_antisymmetrization_le_to_antisymmetrization_iff

added theorem to_antisymmetrization_lt_to_antisymmetrization_iff

added theorem to_antisymmetrization_mono

added theorem to_antisymmetrization_of_antisymmetrization

Modified src/order/category/PartialOrder.lean

added def Preorder_to_PartialOrder

added def Preorder_to_PartialOrder_comp_to_dual_iso_to_dual_comp_Preorder_to_PartialOrder

added def Preorder_to_PartialOrder_forget_adjunction

Modified src/order/rel_classes.lean

modified theorem antisymm'

added theorem antisymm_iff