Note about Mathlib/Init/

The files in Mathlib/Init are leftovers from the port from Mathlib3. (They contain content moved from lean3 itself that Mathlib needed but was not moved to lean4.)

We intend to move all the content of these files out into the main Mathlib directory structure. Contributions assisting with this are appreciated.

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

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