Order instances on quotients

We define a Preorder instance on a general Quotient, as the transitive closure of the x ≤ y ∨ x ≈ y relation. This is the quotient object in the category of preorders.

We show that in the case of a linear order with Set.OrdConnected equivalence classes, this relation is automatically transitive (we don't need to take the transitive closure), and gives a LinearOrder structure on the quotient. In that case, the resulting order is sometimes called a condensation.

instance Quotient.instLE_mathlib {α : Type u_1} {s : Setoid α} [LE α] : LE (Quotient s)

Equations

• Quotient.instLE_mathlib = { le := Quotient.lift₂ (Relation.TransGen fun (x y : α) => x ≤ y ∨ x ≈ y) ⋯ }

theorem Quotient.le_def {α : Type u_1} {s : Setoid α} [LE α] {x y : α} : ⟦x⟧ ≤ ⟦y⟧ ↔ Relation.TransGen (fun (x y : α) => x ≤ y ∨ x ≈ y) x y

instance Quotient.instIsReflLe {α : Type u_1} {s : Setoid α} [LE α] : IsRefl (Quotient s) fun (x1 x2 : Quotient s) => x1 ≤ x2

instance Quotient.instIsTransLe {α : Type u_1} {s : Setoid α} [LE α] : IsTrans (Quotient s) fun (x1 x2 : Quotient s) => x1 ≤ x2

instance Quotient.instIsTotalLe {α : Type u_1} {s : Setoid α} [LE α] [IsTotal α fun (x1 x2 : α) => x1 ≤ x2] : IsTotal (Quotient s) fun (x1 x2 : Quotient s) => x1 ≤ x2

instance Quotient.instPreorder {α : Type u_1} {s : Setoid α} [LE α] : Preorder (Quotient s)

Equations

• Quotient.instPreorder = { toLE := Quotient.instLE_mathlib, lt := fun (a b : Quotient s) => a ≤ b ∧ ¬b ≤ a, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯ }

theorem Quotient.mk_monotone {α : Type u_1} {s : Setoid α} [Preorder α] : Monotone (Quotient.mk s)

theorem Quotient.lift_monotone {α : Type u_2} {β : Type u_3} [Preorder α] {s : Setoid α} [Preorder β] (f : α → β) (hf : Monotone f) (H : ∀ (x₁ x₂ : α), x₁ ≈ x₂ → f x₁ = f x₂) : Monotone (Quotient.lift f H)

theorem Quotient.mk_le_mk {α : Type u_1} {s : Setoid α} [LinearOrder α] [H : ∀ (x : Quotient s), (Quotient.mk s ⁻¹' {x}).OrdConnected] {x y : α} : ⟦x⟧ ≤ ⟦y⟧ ↔ x ≤ y ∨ x ≈ y

instance Quotient.instLinearOrderOfDecidableRelEquiv {α : Type u_1} {s : Setoid α} [LinearOrder α] [H : ∀ (x : Quotient s), (Quotient.mk s ⁻¹' {x}).OrdConnected] [DecidableRel fun (x1 x2 : α) => x1 ≈ x2] : LinearOrder (Quotient s)

Equations

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

theorem Quotient.mk_lt_mk {α : Type u_1} {s : Setoid α} [LinearOrder α] [H : ∀ (x : Quotient s), (Quotient.mk s ⁻¹' {x}).OrdConnected] {x y : α} : ⟦x⟧ < ⟦y⟧ ↔ x < y ∧ ¬x ≈ y

theorem Quotient.lt_of_mk_lt_mk {α : Type u_1} {s : Setoid α} [LinearOrder α] [H : ∀ (x : Quotient s), (Quotient.mk s ⁻¹' {x}).OrdConnected] {x y : α} (h : ⟦x⟧ < ⟦y⟧) : x < y