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 AntisymmRel r is defined so that AntisymmRel r a b ↔ r a b ∧ r b a.

Equations
    Instances For
      theorem antisymmRel_swap {α : Type u_1} (r : ααProp) :
      theorem antisymmRel_swap_apply {α : Type u_1} {a b : α} (r : ααProp) :
      @[simp]
      theorem AntisymmRel.refl {α : Type u_1} (r : ααProp) [IsRefl α r] (a : α) :
      @[deprecated AntisymmRel.refl (since := "2025-01-28")]
      theorem antisymmRel_refl {α : Type u_1} (r : ααProp) [IsRefl α r] (a : α) :

      Alias of AntisymmRel.refl.

      theorem AntisymmRel.rfl {α : Type u_1} {r : ααProp} [IsRefl α r] {a : α} :
      instance instIsReflAntisymmRel {α : Type u_1} (r : ααProp) [IsRefl α r] :
      theorem AntisymmRel.of_eq {α : Type u_1} {r : ααProp} [IsRefl α r] {a b : α} (h : a = b) :
      theorem Eq.antisymmRel {α : Type u_1} {r : ααProp} [IsRefl α r] {a b : α} (h : a = b) :

      Alias of AntisymmRel.of_eq.

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

        Alias of the forward direction of antisymmRel_iff_eq.

        theorem AntisymmRel.le {α : Type u_1} {a b : α} [LE α] (h : AntisymmRel (fun (x1 x2 : α) => x1 x2) a b) :
        a b
        theorem AntisymmRel.ge {α : Type u_1} {a b : α} [LE α] (h : AntisymmRel (fun (x1 x2 : α) => x1 x2) a b) :
        b a
        def AntisymmRel.setoid (α : Type u_1) (r : ααProp) [IsPreorder α r] :

        The antisymmetrization relation as an equivalence relation.

        Equations
          Instances For
            @[simp]
            theorem AntisymmRel.setoid_r (α : Type u_1) (r : ααProp) [IsPreorder α r] (a b : α) :
            (setoid α r) a b = AntisymmRel r a b
            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 le_iff_lt_or_antisymmRel {α : Type u_1} {a b : α} [Preorder α] :
                          a b a < b AntisymmRel (fun (x1 x2 : α) => x1 x2) a b
                          theorem le_of_le_of_antisymmRel {α : Type u_1} {a b c : α} [Preorder α] (h₁ : a b) (h₂ : AntisymmRel (fun (x1 x2 : α) => x1 x2) b c) :
                          a c
                          theorem le_of_antisymmRel_of_le {α : Type u_1} {a b c : α} [Preorder α] (h₁ : AntisymmRel (fun (x1 x2 : α) => x1 x2) a b) (h₂ : b c) :
                          a c
                          theorem lt_of_lt_of_antisymmRel {α : Type u_1} {a b c : α} [Preorder α] (h₁ : a < b) (h₂ : AntisymmRel (fun (x1 x2 : α) => x1 x2) b c) :
                          a < c
                          theorem lt_of_antisymmRel_of_lt {α : Type u_1} {a b c : α} [Preorder α] (h₁ : AntisymmRel (fun (x1 x2 : α) => x1 x2) a b) (h₂ : b < c) :
                          a < c
                          theorem LE.le.lt_or_antisymmRel {α : Type u_1} {a b : α} [Preorder α] :
                          a ba < b AntisymmRel (fun (x1 x2 : α) => x1 x2) a b

                          Alias of the forward direction of le_iff_lt_or_antisymmRel.

                          theorem LE.le.trans_antisymmRel {α : Type u_1} {a b c : α} [Preorder α] (h₁ : a b) (h₂ : AntisymmRel (fun (x1 x2 : α) => x1 x2) b c) :
                          a c

                          Alias of le_of_le_of_antisymmRel.

                          theorem AntisymmRel.trans_le {α : Type u_1} {a b c : α} [Preorder α] (h₁ : AntisymmRel (fun (x1 x2 : α) => x1 x2) a b) (h₂ : b c) :
                          a c

                          Alias of le_of_antisymmRel_of_le.

                          theorem LT.lt.trans_antisymmRel {α : Type u_1} {a b c : α} [Preorder α] (h₁ : a < b) (h₂ : AntisymmRel (fun (x1 x2 : α) => x1 x2) b c) :
                          a < c

                          Alias of lt_of_lt_of_antisymmRel.

                          theorem AntisymmRel.trans_lt {α : Type u_1} {a b c : α} [Preorder α] (h₁ : AntisymmRel (fun (x1 x2 : α) => x1 x2) a b) (h₂ : b < c) :
                          a < c

                          Alias of lt_of_antisymmRel_of_lt.

                          instance instTransLeAntisymmRel {α : Type u_1} [Preorder α] :
                          Trans (fun (x1 x2 : α) => x1 x2) (AntisymmRel fun (x1 x2 : α) => x1 x2) fun (x1 x2 : α) => x1 x2
                          Equations
                            instance instTransAntisymmRelLe {α : Type u_1} [Preorder α] :
                            Trans (AntisymmRel fun (x1 x2 : α) => x1 x2) (fun (x1 x2 : α) => x1 x2) fun (x1 x2 : α) => x1 x2
                            Equations
                              instance instTransLtAntisymmRelLe {α : Type u_1} [Preorder α] :
                              Trans (fun (x1 x2 : α) => x1 < x2) (AntisymmRel fun (x1 x2 : α) => x1 x2) fun (x1 x2 : α) => x1 < x2
                              Equations
                                instance instTransAntisymmRelLeLt {α : Type u_1} [Preorder α] :
                                Trans (AntisymmRel fun (x1 x2 : α) => x1 x2) (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : α) => x1 < x2
                                Equations
                                  theorem AntisymmRel.le_congr {α : Type u_1} {a b c d : α} [Preorder α] (h₁ : AntisymmRel (fun (x1 x2 : α) => x1 x2) a b) (h₂ : AntisymmRel (fun (x1 x2 : α) => x1 x2) c d) :
                                  a c b d
                                  theorem AntisymmRel.le_congr_left {α : Type u_1} {a b c : α} [Preorder α] (h : AntisymmRel (fun (x1 x2 : α) => x1 x2) a b) :
                                  a c b c
                                  theorem AntisymmRel.le_congr_right {α : Type u_1} {a b c : α} [Preorder α] (h : AntisymmRel (fun (x1 x2 : α) => x1 x2) b c) :
                                  a b a c
                                  theorem AntisymmRel.lt_congr {α : Type u_1} {a b c d : α} [Preorder α] (h₁ : AntisymmRel (fun (x1 x2 : α) => x1 x2) a b) (h₂ : AntisymmRel (fun (x1 x2 : α) => x1 x2) c d) :
                                  a < c b < d
                                  theorem AntisymmRel.lt_congr_left {α : Type u_1} {a b c : α} [Preorder α] (h : AntisymmRel (fun (x1 x2 : α) => x1 x2) a b) :
                                  a < c b < c
                                  theorem AntisymmRel.lt_congr_right {α : Type u_1} {a b c : α} [Preorder α] (h : AntisymmRel (fun (x1 x2 : α) => x1 x2) b c) :
                                  a < b a < c
                                  theorem AntisymmRel.antisymmRel_congr {α : Type u_1} {a b c d : α} [Preorder α] (h₁ : AntisymmRel (fun (x1 x2 : α) => x1 x2) a b) (h₂ : AntisymmRel (fun (x1 x2 : α) => x1 x2) c d) :
                                  AntisymmRel (fun (x1 x2 : α) => x1 x2) a c AntisymmRel (fun (x1 x2 : α) => x1 x2) b d
                                  theorem AntisymmRel.antisymmRel_congr_left {α : Type u_1} {a b c : α} [Preorder α] (h : AntisymmRel (fun (x1 x2 : α) => x1 x2) a b) :
                                  AntisymmRel (fun (x1 x2 : α) => x1 x2) a c AntisymmRel (fun (x1 x2 : α) => x1 x2) b c
                                  theorem AntisymmRel.antisymmRel_congr_right {α : Type u_1} {a b c : α} [Preorder α] (h : AntisymmRel (fun (x1 x2 : α) => x1 x2) b c) :
                                  AntisymmRel (fun (x1 x2 : α) => x1 x2) a b AntisymmRel (fun (x1 x2 : α) => x1 x2) a c
                                  theorem AntisymmRel.image {α : Type u_1} {β : Type u_2} {a b : α} [Preorder α] [Preorder β] (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} {a : α} [Preorder α] :
                                    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)
                                    instance instWellFoundedGTAntisymmetrizationLe {α : Type u_1} [Preorder α] [WellFoundedGT α] :
                                    WellFoundedGT (Antisymmetrization α fun (x1 x2 : α) => x1 x2)
                                    instance instLinearOrderAntisymmetrizationLeOfDecidableLEOfDecidableLTOfIsTotal {α : Type u_1} [Preorder α] [DecidableLE α] [DecidableLT α] [IsTotal α fun (x1 x2 : α) => x1 x2] :
                                    LinearOrder (Antisymmetrization α fun (x1 x2 : α) => x1 x2)
                                    Equations
                                      @[simp]
                                      theorem toAntisymmetrization_le_toAntisymmetrization_iff {α : Type u_1} {a b : α} [Preorder α] :
                                      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} {a b : α} [Preorder α] :
                                      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 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 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
                                        Instances For
                                          @[simp]
                                          theorem OrderHom.coe_antisymmetrization {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α →o β) :
                                          theorem OrderHom.antisymmetrization_apply {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α →o β) (a : Antisymmetrization α fun (x1 x2 : α) => x1 x2) :
                                          @[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)
                                          noncomputable def OrderEmbedding.ofAntisymmetrization (α : Type u_1) [Preorder α] :
                                          (Antisymmetrization α fun (x1 x2 : α) => x1 x2) ↪o α

                                          ofAntisymmetrization as an order embedding.

                                          Equations
                                            Instances For
                                              @[simp]
                                              theorem OrderEmbedding.ofAntisymmetrization_apply (α : Type u_1) [Preorder α] (a✝ : Antisymmetrization α fun (x1 x2 : α) => x1 x2) :
                                              (ofAntisymmetrization α) a✝ = _root_.ofAntisymmetrization (fun (x1 x2 : α) => x1 x2) a✝
                                              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 : α) :
                                                  (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 : α) :
                                                  (dualAntisymmetrization α).symm (toAntisymmetrization (fun (x1 x2 : αᵒᵈ) => x1 x2) (OrderDual.toDual a)) = OrderDual.toDual (toAntisymmetrization (fun (x1 x2 : α) => x1 x2) a)
                                                  def Antisymmetrization.prodEquiv (α : Type u_1) (β : Type u_2) [Preorder α] [Preorder β] :
                                                  (Antisymmetrization (α × β) fun (x1 x2 : α × β) => x1 x2) ≃o (Antisymmetrization α fun (x1 x2 : α) => x1 x2) × Antisymmetrization β fun (x1 x2 : β) => x1 x2

                                                  The antisymmetrization of a product preorder is order isomorphic to the product of antisymmetrizations.

                                                  Equations
                                                    Instances For
                                                      @[simp]
                                                      theorem Antisymmetrization.prodEquiv_apply_mk (α : Type u_1) (β : Type u_2) [Preorder α] [Preorder β] {ab : α × β} :
                                                      (prodEquiv α β) ab = (ab.1, ab.2)
                                                      @[simp]
                                                      theorem Antisymmetrization.prodEquiv_symm_apply_mk (α : Type u_1) (β : Type u_2) [Preorder α] [Preorder β] {a : α} {b : β} :
                                                      instance Prod.wellFoundedLT (α : Type u_1) (β : Type u_2) [Preorder α] [Preorder β] [WellFoundedLT α] [WellFoundedLT β] :
                                                      instance Prod.wellFoundedGT (α : Type u_1) (β : Type u_2) [Preorder α] [Preorder β] [WellFoundedGT α] [WellFoundedGT β] :