Theorems · Theorem · category theory

CategoryTheory.Quotient.induction

∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (r : HomRel C)
  {P : {a b : CategoryTheory.Quotient r} → (a ⟶ b) → Prop},
  (∀ {x y : C} (f : x ⟶ y), P ((CategoryTheory.Quotient.functor r).map f)) →
    ∀ {a b : CategoryTheory.Quotient r} (f : a ⟶ b), P f

Defined in

Mathlib.CategoryTheory.Quotient

Cited by

1 results in Mathlib

Foundations

Depth 16 from the axioms · uses propext, Quot.sound

Assumes

CategoryTheory.Category