Documentation

Mathlib.Init.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.

Quot #

Some induction principles tagged with elab_as_elim, since the attribute is missing in core.

@[reducible, inline]
abbrev Quot.recOn' {α : Sort u} {r : ααProp} {motive : Quot rSort v} (q : Quot r) (f : (a : α) → motive (Quot.mk r a)) (h : ∀ (a b : α) (p : r a b), f a = f b) :
motive q

Dependent recursion principle for Quot. This constructor can be tricky to use, so you should consider the simpler versions if they apply:

Equations
Instances For
    @[reducible, inline]
    abbrev Quot.recOnSubsingleton' {α : Sort u} {r : ααProp} {motive : Quot rSort v} [h : ∀ (a : α), Subsingleton (motive (Quot.mk r a))] (q : Quot r) (f : (a : α) → motive (Quot.mk r a)) :
    motive q

    Version of Quot.recOnSubsingleton tagged with elab_as_elim

    Equations
    Instances For
      theorem Quotient.mk'_eq_mk {α : Sort u} [s : Setoid α] :
      Quotient.mk' = Quotient.mk s