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≤ b and b ≤ a≤ 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
theorem antisymmRel_swap {α : Type u_1} (r : ααProp) :
theorem antisymmRel_refl {α : Type u_1} (r : ααProp) [inst : 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} [inst : IsTrans α r] {a : α} {b : α} {c : α} (hab : AntisymmRel r a b) (hbc : AntisymmRel r b c) :
instance AntisymmRel.decidableRel {α : Type u_1} {r : ααProp} [inst : DecidableRel r] :
Equations
@[simp]
theorem antisymmRel_iff_eq {α : Type u_1} {r : ααProp} [inst : IsRefl α r] [inst : IsAntisymm α r] {a : α} {b : α} :
AntisymmRel r a b a = b
theorem AntisymmRel.eq {α : Type u_1} {r : ααProp} [inst : IsRefl α r] [inst : 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) [inst : IsPreorder α r] (a : α) (b : α) :
def AntisymmRel.setoid (α : Type u_1) (r : ααProp) [inst : IsPreorder α r] :

The antisymmetrization relation as an equivalence relation.

Equations
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
def toAntisymmetrization {α : Type u_1} (r : ααProp) [inst : IsPreorder α r] :
αAntisymmetrization α r

Turn an element into its antisymmetrization.

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

Get a representative from the antisymmetrization.

Equations
instance instInhabitedAntisymmetrization {α : Type u_1} (r : ααProp) [inst : IsPreorder α r] [inst : Inhabited α] :
Equations
theorem Antisymmetrization.ind {α : Type u_1} (r : ααProp) [inst : IsPreorder α r] {p : Antisymmetrization α rProp} :
((a : α) → p (toAntisymmetrization r a)) → (q : Antisymmetrization α r) → p q
theorem Antisymmetrization.induction_on {α : Type u_1} (r : ααProp) [inst : IsPreorder α r] {p : Antisymmetrization α rProp} (a : Antisymmetrization α r) (h : (a : α) → p (toAntisymmetrization r a)) :
p a
@[simp]
theorem toAntisymmetrization_ofAntisymmetrization {α : Type u_1} (r : ααProp) [inst : IsPreorder α r] (a : Antisymmetrization α r) :
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)
Equations
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)
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
Equations
  • One or more equations did not get rendered due to their size.
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.
@[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
@[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
@[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
@[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
theorem toAntisymmetrization_mono {α : Type u_1} [inst : Preorder α] :
Monotone (toAntisymmetrization fun x x_1 => x x_1)
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.
@[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)
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
@[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)
@[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
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.
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.
@[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)
@[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)