Documentation

Mathlib.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 AntisymmRel {α : Type u_1} (r : ααProp) (a : α) (b : α) :

The antisymmetrization relation.

Equations
Instances For
    theorem antisymmRel_swap {α : Type u_1} (r : ααProp) :
    theorem antisymmRel_refl {α : Type u_1} (r : ααProp) [IsRefl α r] (a : α) :
    theorem AntisymmRel.symm {α : Type u_1} {r : ααProp} {a : α} {b : α} :
    AntisymmRel r a bAntisymmRel r b a
    theorem AntisymmRel.trans {α : Type u_1} {r : ααProp} [IsTrans α r] {a : α} {b : α} {c : α} (hab : AntisymmRel r a b) (hbc : AntisymmRel r b c) :
    instance AntisymmRel.decidableRel {α : Type u_1} {r : ααProp} [DecidableRel r] :
    Equations
    @[simp]
    theorem antisymmRel_iff_eq {α : Type u_1} {r : ααProp} [IsRefl α r] [IsAntisymm α r] {a : α} {b : α} :
    AntisymmRel r a b a = b
    theorem AntisymmRel.eq {α : Type u_1} {r : ααProp} [IsRefl α r] [IsAntisymm α r] {a : α} {b : α} :
    AntisymmRel r a ba = b

    Alias of the forward direction of antisymmRel_iff_eq.

    @[simp]
    theorem AntisymmRel.setoid_r (α : Type u_1) (r : ααProp) [IsPreorder α r] (a : α) (b : α) :
    def AntisymmRel.setoid (α : Type u_1) (r : ααProp) [IsPreorder α r] :

    The antisymmetrization relation as an equivalence relation.

    Equations
    Instances For
      def Antisymmetrization (α : Type u_1) (r : ααProp) [IsPreorder α r] :
      Type u_1

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

      Equations
      Instances For
        def toAntisymmetrization {α : Type u_1} (r : ααProp) [IsPreorder α r] :
        αAntisymmetrization α r

        Turn an element into its antisymmetrization.

        Equations
        Instances For
          noncomputable def ofAntisymmetrization {α : Type u_1} (r : ααProp) [IsPreorder α r] :
          Antisymmetrization α rα

          Get a representative from the antisymmetrization.

          Equations
          Instances For
            instance instInhabitedAntisymmetrization {α : Type u_1} (r : ααProp) [IsPreorder α r] [Inhabited α] :
            Equations
            theorem Antisymmetrization.ind {α : Type u_1} (r : ααProp) [IsPreorder α r] {p : Antisymmetrization α rProp} :
            (∀ (a : α), p (toAntisymmetrization r a))∀ (q : Antisymmetrization α r), p q
            theorem Antisymmetrization.induction_on {α : Type u_1} (r : ααProp) [IsPreorder α r] {p : Antisymmetrization α rProp} (a : Antisymmetrization α r) (h : ∀ (a : α), p (toAntisymmetrization r a)) :
            p a
            @[simp]
            theorem AntisymmRel.image {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {a : α} {b : α} (h : AntisymmRel (fun (x1 x2 : α) => x1 x2) a b) {f : αβ} (hf : Monotone f) :
            AntisymmRel (fun (x1 x2 : β) => x1 x2) (f a) (f b)
            instance instPartialOrderAntisymmetrization {α : Type u_1} [Preorder α] :
            PartialOrder (Antisymmetrization α fun (x1 x2 : α) => x1 x2)
            Equations
            theorem antisymmetrization_fibration {α : Type u_1} [Preorder α] :
            Relation.Fibration (fun (x1 x2 : α) => x1 < x2) (fun (x1 x2 : Antisymmetrization α fun (x1 x2 : α) => x1 x2) => x1 < x2) (toAntisymmetrization fun (x1 x2 : α) => x1 x2)
            theorem acc_antisymmetrization_iff {α : Type u_1} [Preorder α] {a : α} :
            Acc (fun (x1 x2 : Antisymmetrization α fun (x1 x2 : α) => x1 x2) => x1 < x2) (toAntisymmetrization (fun (x1 x2 : α) => x1 x2) a) Acc (fun (x1 x2 : α) => x1 < x2) a
            instance instWellFoundedLTAntisymmetrizationLe {α : Type u_1} [Preorder α] [WellFoundedLT α] :
            WellFoundedLT (Antisymmetrization α fun (x1 x2 : α) => x1 x2)
            Equations
            • =
            instance instLinearOrderAntisymmetrizationLeOfDecidableRelLtOfIsTotal {α : Type u_1} [Preorder α] [DecidableRel fun (x1 x2 : α) => x1 x2] [DecidableRel fun (x1 x2 : α) => x1 < x2] [IsTotal α fun (x1 x2 : α) => x1 x2] :
            LinearOrder (Antisymmetrization α fun (x1 x2 : α) => x1 x2)
            Equations
            • One or more equations did not get rendered due to their size.
            @[simp]
            theorem toAntisymmetrization_le_toAntisymmetrization_iff {α : Type u_1} [Preorder α] {a : α} {b : α} :
            toAntisymmetrization (fun (x1 x2 : α) => x1 x2) a toAntisymmetrization (fun (x1 x2 : α) => x1 x2) b a b
            @[simp]
            theorem toAntisymmetrization_lt_toAntisymmetrization_iff {α : Type u_1} [Preorder α] {a : α} {b : α} :
            toAntisymmetrization (fun (x1 x2 : α) => x1 x2) a < toAntisymmetrization (fun (x1 x2 : α) => x1 x2) b a < b
            @[simp]
            theorem ofAntisymmetrization_le_ofAntisymmetrization_iff {α : Type u_1} [Preorder α] {a : Antisymmetrization α fun (x1 x2 : α) => x1 x2} {b : Antisymmetrization α fun (x1 x2 : α) => x1 x2} :
            ofAntisymmetrization (fun (x1 x2 : α) => x1 x2) a ofAntisymmetrization (fun (x1 x2 : α) => x1 x2) b a b
            @[simp]
            theorem ofAntisymmetrization_lt_ofAntisymmetrization_iff {α : Type u_1} [Preorder α] {a : Antisymmetrization α fun (x1 x2 : α) => x1 x2} {b : Antisymmetrization α fun (x1 x2 : α) => x1 x2} :
            ofAntisymmetrization (fun (x1 x2 : α) => x1 x2) a < ofAntisymmetrization (fun (x1 x2 : α) => x1 x2) b a < b
            theorem toAntisymmetrization_mono {α : Type u_1} [Preorder α] :
            Monotone (toAntisymmetrization fun (x1 x2 : α) => x1 x2)
            def OrderHom.antisymmetrization {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α →o β) :
            (Antisymmetrization α fun (x1 x2 : α) => x1 x2) →o Antisymmetrization β fun (x1 x2 : β) => x1 x2

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

            Equations
            • f.antisymmetrization = { toFun := Quotient.map' f , monotone' := }
            Instances For
              @[simp]
              theorem OrderHom.coe_antisymmetrization {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α →o β) :
              f.antisymmetrization = Quotient.map' f
              theorem OrderHom.antisymmetrization_apply {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α →o β) (a : Antisymmetrization α fun (x1 x2 : α) => x1 x2) :
              f.antisymmetrization a = Quotient.map' f a
              @[simp]
              theorem OrderHom.antisymmetrization_apply_mk {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α →o β) (a : α) :
              f.antisymmetrization (toAntisymmetrization (fun (x1 x2 : α) => x1 x2) a) = toAntisymmetrization (fun (x1 x2 : β) => x1 x2) (f a)
              @[simp]
              theorem OrderEmbedding.ofAntisymmetrization_apply (α : Type u_1) [Preorder α] :
              ∀ (a : Antisymmetrization α fun (x1 x2 : α) => x1 x2), (OrderEmbedding.ofAntisymmetrization α) a = ofAntisymmetrization (fun (x1 x2 : α) => x1 x2) a
              noncomputable def OrderEmbedding.ofAntisymmetrization (α : Type u_1) [Preorder α] :
              (Antisymmetrization α fun (x1 x2 : α) => x1 x2) ↪o α

              ofAntisymmetrization as an order embedding.

              Equations
              Instances For
                def OrderIso.dualAntisymmetrization (α : Type u_1) [Preorder α] :
                (Antisymmetrization α fun (x1 x2 : α) => x1 x2)ᵒᵈ ≃o Antisymmetrization αᵒᵈ fun (x1 x2 : αᵒᵈ) => x1 x2

                Antisymmetrization and orderDual commute.

                Equations
                Instances For
                  @[simp]
                  theorem OrderIso.dualAntisymmetrization_apply (α : Type u_1) [Preorder α] (a : α) :
                  (OrderIso.dualAntisymmetrization α) (OrderDual.toDual (toAntisymmetrization (fun (x1 x2 : α) => x1 x2) a)) = toAntisymmetrization (fun (x1 x2 : αᵒᵈ) => x1 x2) (OrderDual.toDual a)
                  @[simp]
                  theorem OrderIso.dualAntisymmetrization_symm_apply (α : Type u_1) [Preorder α] (a : α) :
                  (OrderIso.dualAntisymmetrization α).symm (toAntisymmetrization (fun (x1 x2 : αᵒᵈ) => x1 x2) (OrderDual.toDual a)) = OrderDual.toDual (toAntisymmetrization (fun (x1 x2 : α) => x1 x2) a)