Theorems · Definition · category theory

CategoryTheory.IsCofiltered.cofilteredClosure.below.casesOn

∀ {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}
  {motive_1 :
    {a : C} →
      (t : CategoryTheory.IsCofiltered.cofilteredClosure f a) →
        CategoryTheory.IsCofiltered.cofilteredClosure.below t → Prop}
  {a : C} {t : CategoryTheory.IsCofiltered.cofilteredClosure f a}
  (t_1 : CategoryTheory.IsCofiltered.cofilteredClosure.below t),
  (∀ (x : α), motive_1 ⋯ ⋯) →
    (∀ {j j' : C} (a : CategoryTheory.IsCofiltered.cofilteredClosure f j)
        (a_1 : CategoryTheory.IsCofiltered.cofilteredClosure f j')
        (ih : CategoryTheory.IsCofiltered.cofilteredClosure.below a) (a_ih : motive j a)
        (ih_1 : CategoryTheory.IsCofiltered.cofilteredClosure.below a_1) (a_ih_1 : motive j' a_1), motive_1 ⋯ ⋯) →
      (∀ {j j' : C} (a : CategoryTheory.IsCofiltered.cofilteredClosure f j)
          (a_1 : CategoryTheory.IsCofiltered.cofilteredClosure f j') (f_1 f' : j ⟶ j')
          (ih : CategoryTheory.IsCofiltered.cofilteredClosure.below a) (a_ih : motive j a)
          (ih_1 : CategoryTheory.IsCofiltered.cofilteredClosure.below a_1) (a_ih_1 : motive j' a_1), motive_1 ⋯ ⋯) →
        motive_1 t t_1

Defined in

Mathlib.CategoryTheory.Filtered.Small

Cited by

0 results in Mathlib

Foundations

Depth 13 from the axioms · uses Classical.choice

Assumes

CategoryTheory.CategoryCategoryTheory.IsCofilteredOrEmpty