Quotient types

These are ported from the Lean 3 standard library file init/data/quot.lean.

inductive EqvGen {α : Type u} (r : α → α → Prop) : α → α → Prop

EqvGen r is the equivalence relation generated by r.

• rel: ∀ {α : Type u} {r : α → α → Prop} (x y : α), r x y → EqvGen r x y
• refl: ∀ {α : Type u} {r : α → α → Prop} (x : α), EqvGen r x x
• symm: ∀ {α : Type u} {r : α → α → Prop} (x y : α), EqvGen r x y → EqvGen r y x
• trans: ∀ {α : Type u} {r : α → α → Prop} (x y z : α), EqvGen r x y → EqvGen r y z → EqvGen r x z

theorem EqvGen.is_equivalence {α : Type u} (r : α → α → Prop) : Equivalence (EqvGen r)

def EqvGen.Setoid {α : Type u} (r : α → α → Prop) : Setoid α

EqvGen.Setoid r is the setoid generated by a relation r.

The motivation for this definition is that Quot r behaves like Quotient (EqvGen.Setoid r), see for example Quot.exact and Quot.EqvGen_sound.

Equations

• EqvGen.Setoid r = { r := EqvGen r, iseqv := ⋯ }

theorem Quot.exact {α : Type u} (r : α → α → Prop) {a : α} {b : α} (H : Quot.mk r a = Quot.mk r b) : EqvGen r a b

theorem Quot.EqvGen_sound {α : Type u} {r : α → α → Prop} {a : α} {b : α} (H : EqvGen r a b) : Quot.mk r a = Quot.mk r b

instance Quotient.decidableEq {α : Sort u} {s : Setoid α} [d : (a b : α) → Decidable (a ≈ b)] : DecidableEq (Quotient s)

Equations

• Quotient.decidableEq q₁ q₂ = Quotient.recOnSubsingleton₂ q₁ q₂ fun (a₁ a₂ : α) => match d a₁ a₂ with | isTrue h₁ => isTrue ⋯ | isFalse h₂ => isFalse ⋯