Documentation

Mathlib.Init.Quot

Quot #

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

@[inline, reducible]
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
    @[inline, reducible]
    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