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≤ b and b ≤ a≤ a.

Antisymmetrization is a functor from Preorder to PartialOrder. See Preorder_to_PartialOrder.

Main declarations

• AntisymmRel: The antisymmetrization relation. AntisymmRel r a b means that a and b are related both ways by r.
• Antisymmetrization α r: The quotient of α by AntisymmRel r. Even when r is just a preorder, Antisymmetrization α is a partial order.

ink

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

The antisymmetrization relation.

Equations

• AntisymmRel r a b = (r a b ∧ r b a)

ink

theorem antisymmRel_swap {α : Type u_1} (r : α → α → Prop) : AntisymmRel (Function.swap r) = AntisymmRel r

ink

theorem antisymmRel_refl {α : Type u_1} (r : α → α → Prop) [inst : IsRefl α r] (a : α) : AntisymmRel r a a

ink

theorem AntisymmRel.symm {α : Type u_1} {r : α → α → Prop} {a : α} {b : α} : AntisymmRel r a b → AntisymmRel r b a

ink

theorem AntisymmRel.trans {α : Type u_1} {r : α → α → Prop} [inst : IsTrans α r] {a : α} {b : α} {c : α} (hab : AntisymmRel r a b) (hbc : AntisymmRel r b c) : AntisymmRel r a c

ink

instance AntisymmRel.decidableRel {α : Type u_1} {r : α → α → Prop} [inst : DecidableRel r] : DecidableRel (AntisymmRel r)

Equations

• AntisymmRel.decidableRel x x = instDecidableAnd

ink

@[simp]

theorem antisymmRel_iff_eq {α : Type u_1} {r : α → α → Prop} [inst : IsRefl α r] [inst : IsAntisymm α r] {a : α} {b : α} : AntisymmRel r a b ↔ a = b

ink

theorem AntisymmRel.eq {α : Type u_1} {r : α → α → Prop} [inst : IsRefl α r] [inst : IsAntisymm α r] {a : α} {b : α} : AntisymmRel r a b → a = b

Alias of the forward direction of antisymmRel_iff_eq.

ink

@[simp]

theorem AntisymmRel.setoid_r (α : Type u_1) (r : α → α → Prop) [inst : IsPreorder α r] (a : α) (b : α) : Setoid.r a b = AntisymmRel r a b

ink

def AntisymmRel.setoid (α : Type u_1) (r : α → α → Prop) [inst : IsPreorder α r] : Setoid α

The antisymmetrization relation as an equivalence relation.

Equations

• AntisymmRel.setoid α r = { r := AntisymmRel r, iseqv := (_ : Equivalence (AntisymmRel r)) }

ink

def Antisymmetrization (α : Type u_1) (r : α → α → Prop) [inst : 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≤ b ∧ b ≤ a∧ b ≤ a≤ a.

Equations

• Antisymmetrization α r = Quotient (AntisymmRel.setoid α r)

ink

def toAntisymmetrization {α : Type u_1} (r : α → α → Prop) [inst : IsPreorder α r] : α → Antisymmetrization α r

Turn an element into its antisymmetrization.

Equations

• toAntisymmetrization r = Quotient.mk (AntisymmRel.setoid α r)

ink

noncomputable def ofAntisymmetrization {α : Type u_1} (r : α → α → Prop) [inst : IsPreorder α r] : Antisymmetrization α r → α

Get a representative from the antisymmetrization.

Equations

• ofAntisymmetrization r = Quotient.out'

ink

instance instInhabitedAntisymmetrization {α : Type u_1} (r : α → α → Prop) [inst : IsPreorder α r] [inst : Inhabited α] : Inhabited (Antisymmetrization α r)

Equations

• instInhabitedAntisymmetrization r = id inferInstance

ink

theorem Antisymmetrization.ind {α : Type u_1} (r : α → α → Prop) [inst : IsPreorder α r] {p : Antisymmetrization α r → Prop} : ((a : α) → p (toAntisymmetrization r a)) → (q : Antisymmetrization α r) → p q

ink

theorem Antisymmetrization.induction_on {α : Type u_1} (r : α → α → Prop) [inst : IsPreorder α r] {p : Antisymmetrization α r → Prop} (a : Antisymmetrization α r) (h : (a : α) → p (toAntisymmetrization r a)) : p a

ink

@[simp]

theorem toAntisymmetrization_ofAntisymmetrization {α : Type u_1} (r : α → α → Prop) [inst : IsPreorder α r] (a : Antisymmetrization α r) : toAntisymmetrization r (ofAntisymmetrization r a) = a

ink

theorem AntisymmRel.image {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] {a : α} {b : α} (h : AntisymmRel (fun x x_1 => x ≤ x_1) a b) {f : α → β} (hf : Monotone f) : AntisymmRel (fun x x_1 => x ≤ x_1) (f a) (f b)

ink

instance instPartialOrderAntisymmetrizationLeToLEInstIsPreorderLeToLE {α : Type u_1} [inst : Preorder α] : PartialOrder (Antisymmetrization α fun x x_1 => x ≤ x_1)

Equations

• instPartialOrderAntisymmetrizationLeToLEInstIsPreorderLeToLE = PartialOrder.mk (_ : ∀ (a b : Antisymmetrization α fun x x_1 => x ≤ x_1), a ≤ b → b ≤ a → a = b)

ink

theorem antisymmetrization_fibration {α : Type u_1} [inst : Preorder α] : Relation.Fibration (fun x x_1 => x < x_1) (fun x x_1 => x < x_1) (toAntisymmetrization fun x x_1 => x ≤ x_1)

ink

theorem acc_antisymmetrization_iff {α : Type u_1} [inst : Preorder α] {a : α} : Acc (fun x x_1 => x < x_1) (toAntisymmetrization (fun x x_1 => x ≤ x_1) a) ↔ Acc (fun x x_1 => x < x_1) a

ink

theorem wellFounded_antisymmetrization_iff {α : Type u_1} [inst : Preorder α] : WellFounded LT.lt ↔ WellFounded LT.lt

ink

instance instWellFoundedLTAntisymmetrizationLeToLEInstIsPreorderLeToLEToLTToPreorderInstPartialOrderAntisymmetrizationLeToLEInstIsPreorderLeToLE {α : Type u_1} [inst : Preorder α] [inst : WellFoundedLT α] : WellFoundedLT (Antisymmetrization α fun x x_1 => x ≤ x_1)

Equations

• One or more equations did not get rendered due to their size.

ink

instance instLinearOrderAntisymmetrizationLeToLEInstIsPreorderLeToLE {α : Type u_1} [inst : Preorder α] [inst : DecidableRel fun x x_1 => x ≤ x_1] [inst : DecidableRel fun x x_1 => x < x_1] [inst : IsTotal α fun x x_1 => x ≤ x_1] : LinearOrder (Antisymmetrization α fun x x_1 => x ≤ x_1)

Equations

• One or more equations did not get rendered due to their size.

ink

@[simp]

theorem toAntisymmetrization_le_toAntisymmetrization_iff {α : Type u_1} [inst : Preorder α] {a : α} {b : α} : toAntisymmetrization (fun x x_1 => x ≤ x_1) a ≤ toAntisymmetrization (fun x x_1 => x ≤ x_1) b ↔ a ≤ b

ink

@[simp]

theorem toAntisymmetrization_lt_toAntisymmetrization_iff {α : Type u_1} [inst : Preorder α] {a : α} {b : α} : toAntisymmetrization (fun x x_1 => x ≤ x_1) a < toAntisymmetrization (fun x x_1 => x ≤ x_1) b ↔ a < b

ink

@[simp]

theorem ofAntisymmetrization_le_ofAntisymmetrization_iff {α : Type u_1} [inst : Preorder α] {a : Antisymmetrization α fun x x_1 => x ≤ x_1} {b : Antisymmetrization α fun x x_1 => x ≤ x_1} : ofAntisymmetrization (fun x x_1 => x ≤ x_1) a ≤ ofAntisymmetrization (fun x x_1 => x ≤ x_1) b ↔ a ≤ b

ink

@[simp]

theorem ofAntisymmetrization_lt_ofAntisymmetrization_iff {α : Type u_1} [inst : Preorder α] {a : Antisymmetrization α fun x x_1 => x ≤ x_1} {b : Antisymmetrization α fun x x_1 => x ≤ x_1} : ofAntisymmetrization (fun x x_1 => x ≤ x_1) a < ofAntisymmetrization (fun x x_1 => x ≤ x_1) b ↔ a < b

ink

theorem toAntisymmetrization_mono {α : Type u_1} [inst : Preorder α] : Monotone (toAntisymmetrization fun x x_1 => x ≤ x_1)

ink

def OrderHom.antisymmetrization {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] (f : α →o β) : (Antisymmetrization α fun x x_1 => x ≤ x_1) →o Antisymmetrization β fun x x_1 => x ≤ x_1

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

Equations

• One or more equations did not get rendered due to their size.

ink

@[simp]

theorem OrderHom.coe_antisymmetrization {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] (f : α →o β) : ↑(OrderHom.antisymmetrization f) = Quotient.map' ↑f (_ : (Setoid.r ⇒ Setoid.r) ↑f ↑f)

ink

theorem OrderHom.antisymmetrization_apply {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] (f : α →o β) (a : Antisymmetrization α fun x x_1 => x ≤ x_1) : ↑(OrderHom.antisymmetrization f) a = Quotient.map' ↑f (_ : (Setoid.r ⇒ Setoid.r) ↑f ↑f) a

ink

@[simp]

theorem OrderHom.antisymmetrization_apply_mk {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] (f : α →o β) (a : α) : ↑(OrderHom.antisymmetrization f) (toAntisymmetrization (fun x x_1 => x ≤ x_1) a) = toAntisymmetrization (fun x x_1 => x ≤ x_1) (↑f a)

ink

@[simp]

theorem OrderEmbedding.ofAntisymmetrization_apply (α : Type u_1) [inst : Preorder α] : ∀ (a : Antisymmetrization α fun x x_1 => x ≤ x_1), ↑(OrderEmbedding.ofAntisymmetrization α).toEmbedding a = ofAntisymmetrization (fun x x_1 => x ≤ x_1) a

ink

noncomputable def OrderEmbedding.ofAntisymmetrization (α : Type u_1) [inst : Preorder α] : (Antisymmetrization α fun x x_1 => x ≤ x_1) ↪o α

ofAntisymmetrization as an order embedding.

Equations

• One or more equations did not get rendered due to their size.

ink

def OrderIso.dualAntisymmetrization (α : Type u_1) [inst : Preorder α] : (Antisymmetrization α fun x x_1 => x ≤ x_1)ᵒᵈ ≃o Antisymmetrization αᵒᵈ fun x x_1 => x ≤ x_1

Antisymmetrization and orderDual commute.

Equations

• One or more equations did not get rendered due to their size.

ink

@[simp]

theorem OrderIso.dualAntisymmetrization_apply (α : Type u_1) [inst : Preorder α] (a : α) : ↑(RelIso.toRelEmbedding (OrderIso.dualAntisymmetrization α)).toEmbedding (↑OrderDual.toDual (toAntisymmetrization (fun x x_1 => x ≤ x_1) a)) = toAntisymmetrization (fun x x_1 => x ≤ x_1) (↑OrderDual.toDual a)

ink

@[simp]

theorem OrderIso.dualAntisymmetrization_symm_apply (α : Type u_1) [inst : Preorder α] (a : α) : ↑(RelIso.toRelEmbedding (OrderIso.symm (OrderIso.dualAntisymmetrization α))).toEmbedding (toAntisymmetrization (fun x x_1 => x ≤ x_1) (↑OrderDual.toDual a)) = ↑OrderDual.toDual (toAntisymmetrization (fun x x_1 => x ≤ x_1) a)