Theorems · Definition · category theory

CategoryTheory.IsCofiltered.cofilteredClosure.recOn

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsCofilteredOrEmpty C] {α : Type w}
  {f : α → C} {motive : (a : C) → CategoryTheory.IsCofiltered.cofilteredClosure f a → Prop} {a : C}
  (t : CategoryTheory.IsCofiltered.cofilteredClosure f a),
  (∀ (x : α), motive (f x) ⋯) →
    (∀ {j j' : C} (a : CategoryTheory.IsCofiltered.cofilteredClosure f j)
        (a_1 : CategoryTheory.IsCofiltered.cofilteredClosure f j'),
        motive j a → motive j' a_1 → motive (CategoryTheory.IsCofiltered.min j j') ⋯) →
      (∀ {j j' : C} (a : CategoryTheory.IsCofiltered.cofilteredClosure f j)
          (a_1 : CategoryTheory.IsCofiltered.cofilteredClosure f j') (f_1 f' : j ⟶ j'),
          motive j a → motive j' a_1 → motive (CategoryTheory.IsCofiltered.eq f_1 f') ⋯) →
        motive a t

Defined in

Mathlib.CategoryTheory.Filtered.Small

Cited by

0 results in Mathlib

Foundations

Depth 12 from the axioms · uses Classical.choice

Assumes

CategoryTheory.CategoryCategoryTheory.IsCofilteredOrEmpty