def Preorder.toSetoid {α : Type u_1} (p : Preorder α) : Setoid α

Equations

• p.toSetoid = { r := fun (x y : α) => x ≤ y ∧ y ≤ x, iseqv := ⋯ }

theorem Preorder.equiv_iff {α : Type u_1} (p : Preorder α) (x y : α) : let x_1 := p.toSetoid; x ≈ y ↔ x ≤ y ∧ y ≤ x

def OrderQuotient {α : Type u_1} (p : Preorder α) : Type u_1

Equations

• OrderQuotient p = Quotient p.toSetoid

instance OrderQuotient.partialOrder {α : Type u_1} (p : Preorder α) : PartialOrder (OrderQuotient p)

Equations

• OrderQuotient.partialOrder p = { le := Quotient.lift₂ LE.le ⋯, lt := Quotient.lift₂ LT.lt ⋯, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_le := ⋯, le_antisymm := ⋯ }

def Preorder.quotient {α : Type u_1} (p : Preorder α) (x : α) : OrderQuotient p

Equations

• p.quotient x = Quotient.mk p.toSetoid x

theorem Preorder.quot_eq_iff {α : Type u_1} (p : Preorder α) (x y : α) : let x_1 := p.toSetoid; p.quotient x = p.quotient y ↔ x ≈ y

theorem Quotient.liftBeta {α : Sort u} {s : Setoid α} {β : Sort v} (f : α → β) (c : ∀ (a b : α), a ≈ b → f a = f b) (a : α) : Quotient.lift f c (Quotient.mk s a) = f a

for Mathlib? -

theorem Quotient.lift₂Beta {α : Sort uA} {β : Sort uB} {φ : Sort uC} {s₁ : Setoid α} {s₂ : Setoid β} (f : α → β → φ) (c : ∀ (a₁ : α) (b₁ : β) (a₂ : α) (b₂ : β), a₁ ≈ a₂ → b₁ ≈ b₂ → f a₁ b₁ = f a₂ b₂) (a : α) (b : β) : Quotient.lift₂ f c (Quotient.mk s₁ a) (Quotient.mk s₂ b) = f a b

for Mathlib? -

theorem Preorder.quot_le_iff {α : Type u_1} (p : Preorder α) (x y : α) : p.quotient x ≤ p.quotient y ↔ x ≤ y

theorem Preorder.quot_lt_iff {α : Type u_1} (p : Preorder α) (x y : α) : p.quotient x < p.quotient y ↔ x < y

noncomputable def Preorder.quot_linear {α : Type u_1} (p : Preorder α) (h : ∀ (x y : α), x ≤ y ∨ y ≤ x) : LinearOrder (OrderQuotient p)

Equations

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