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

• 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.

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

The antisymmetrization relation AntisymmRel r is defined so that AntisymmRel r a b ↔ r a b ∧ r b a.

Equations

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

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

theorem antisymmRel_swap_apply {α : Type u_1} {a b : α} (r : α → α → Prop) : AntisymmRel (Function.swap r) a b ↔ AntisymmRel r a b

@[simp]

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

theorem AntisymmRel.rfl {α : Type u_1} {r : α → α → Prop} [IsRefl α r] {a : α} : AntisymmRel r a a

instance instIsReflAntisymmRel {α : Type u_1} (r : α → α → Prop) [IsRefl α r] : IsRefl α (AntisymmRel r)

theorem AntisymmRel.of_eq {α : Type u_1} {r : α → α → Prop} [IsRefl α r] {a b : α} (h : a = b) : AntisymmRel r a b

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

Alias of AntisymmRel.of_eq.

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

instance instIsSymmAntisymmRel {α : Type u_1} {r : α → α → Prop} : IsSymm α (AntisymmRel r)

theorem antisymmRel_comm {α : Type u_1} {a b : α} {r : α → α → Prop} : AntisymmRel r a b ↔ AntisymmRel r b a

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

instance instIsTransAntisymmRel {α : Type u_1} {r : α → α → Prop} [IsTrans α r] : IsTrans α (AntisymmRel r)

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

Equations

• AntisymmRel.decidableRel x✝¹ x✝ = instDecidableAnd

@[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 b → a = b

Alias of the forward direction of antisymmRel_iff_eq.

theorem Mathlib.Tactic.GCongr.AntisymmRel.left {α : Type u_3} {a b : α} {r : α → α → Prop} (h : AntisymmRel r a b) : r a b

theorem Mathlib.Tactic.GCongr.AntisymmRel.right {α : Type u_3} {a b : α} {r : α → α → Prop} (h : AntisymmRel r a b) : r b a

def Mathlib.Tactic.GCongr.exactAntisymmRelLeft : ForwardExt

See if the term is AntisymmRel r a b and the goal is r a b.

Equations

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

def Mathlib.Tactic.GCongr.exactAntisymmRelRight : ForwardExt

See if the term is AntisymmRel r a b and the goal is r b a.

Equations

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

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] : Setoid α

The antisymmetrization relation as an equivalence relation.

Equations

• AntisymmRel.setoid α r = { r := AntisymmRel r, iseqv := ⋯ }

@[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

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

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

Turn an element into its antisymmetrization.

Equations

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

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

Get a representative from the antisymmetrization.

Equations

• ofAntisymmetrization r = Quotient.out

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

Equations

• instInhabitedAntisymmetrization r = id inferInstance

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

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

@[simp]

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

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 ≤ b → a < 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

• instTransLeAntisymmRel = { trans := ⋯ }

instance instTransAntisymmRelLe {α : Type u_1} [Preorder α] : Trans (AntisymmRel fun (x1 x2 : α) => x1 ≤ x2) (fun (x1 x2 : α) => x1 ≤ x2) fun (x1 x2 : α) => x1 ≤ x2

Equations

• instTransAntisymmRelLe = { trans := ⋯ }

instance instTransLtAntisymmRelLe {α : Type u_1} [Preorder α] : Trans (fun (x1 x2 : α) => x1 < x2) (AntisymmRel fun (x1 x2 : α) => x1 ≤ x2) fun (x1 x2 : α) => x1 < x2

Equations

• instTransLtAntisymmRelLe = { trans := ⋯ }

instance instTransAntisymmRelLeLt {α : Type u_1} [Preorder α] : Trans (AntisymmRel fun (x1 x2 : α) => x1 ≤ x2) (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : α) => x1 < x2

Equations

• instTransAntisymmRelLeLt = { trans := ⋯ }

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

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

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

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

theorem wellFoundedLT_antisymmetrization_iff {α : Type u_1} [Preorder α] : WellFoundedLT (Antisymmetrization α fun (x1 x2 : α) => x1 ≤ x2) ↔ WellFoundedLT α

theorem wellFoundedGT_antisymmetrization_iff {α : Type u_1} [Preorder α] : WellFoundedGT (Antisymmetrization α fun (x1 x2 : α) => x1 ≤ x2) ↔ WellFoundedGT α

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

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

@[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

• f.antisymmetrization = { toFun := Quotient.map' ⇑f ⋯, monotone' := ⋯ }

@[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)

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

ofAntisymmetrization as an order embedding.

Equations

• OrderEmbedding.ofAntisymmetrization α = { toFun := ofAntisymmetrization fun (x1 x2 : α) => x1 ≤ x2, inj' := ⋯, map_rel_iff' := ⋯ }

@[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

• OrderIso.dualAntisymmetrization α = { toFun := Quotient.map' id ⋯, invFun := Quotient.map' id ⋯, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }

@[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

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

@[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 : β} : (prodEquiv α β).symm (⟦a⟧, ⟦b⟧) = ⟦(a, b)⟧

instance Prod.wellFoundedLT (α : Type u_1) (β : Type u_2) [Preorder α] [Preorder β] [WellFoundedLT α] [WellFoundedLT β] : WellFoundedLT (α × β)

instance Prod.wellFoundedGT (α : Type u_1) (β : Type u_2) [Preorder α] [Preorder β] [WellFoundedGT α] [WellFoundedGT β] : WellFoundedGT (α × β)