Documentation

Mathlib.Init.Data.Quot

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.

Instances For
    theorem EqvGen.is_equivalence {α : Type u} (r : ααProp) :
    def EqvGen.Setoid {α : Type u} (r : ααProp) :

    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.eqvGen_exact and Quot.eqvGen_sound.

    Equations
    Instances For
      theorem Quot.eqvGen_exact {α : Type u} (r : ααProp) {a : α} {b : α} (H : Quot.mk r a = Quot.mk r b) :
      EqvGen r a b
      @[deprecated Quot.eqvGen_exact]
      theorem Quot.exact {α : Type u} (r : ααProp) {a : α} {b : α} (H : Quot.mk r a = Quot.mk r b) :
      EqvGen r a b

      Alias of Quot.eqvGen_exact.

      theorem Quot.eqvGen_sound {α : Type u} {r : ααProp} {a : α} {b : α} (H : EqvGen r a b) :
      Quot.mk r a = Quot.mk r b
      @[deprecated Quot.eqvGen_sound]
      theorem Quot.EqvGen_sound {α : Type u} {r : ααProp} {a : α} {b : α} (H : EqvGen r a b) :
      Quot.mk r a = Quot.mk r b

      Alias of Quot.eqvGen_sound.

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