Theorems · Definition · category theory

CategoryTheory.Presieve.singleton.casesOn

{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : C} →
      {f : Y ⟶ X} →
        {motive : ⦃Y_1 : C⦄ → (a : Y_1 ⟶ X) → CategoryTheory.Presieve.singleton f a → Sort u} →
          ⦃Y_1 : C⦄ → {a : Y_1 ⟶ X} → (t : CategoryTheory.Presieve.singleton f a) → motive f ⋯ → motive a t

Defined in: Mathlib.CategoryTheory.Sites.Sieves
Cited by: 9 results in Mathlib
Foundations: Depth 6 from the axioms · uses no axioms
Assumes: CategoryTheory.Category

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites3

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

CategoryTheory.Categorystatement and proof · cited by 32,673
Quiver.Homstatement and proof · cited by 32,603
CategoryTheory.Presieve.singletonstatement and proof · cited by 57

Cited by9

Results whose statement or proof uses this declaration.

CategoryTheory.Sieve.generateSingleton_eqproof · cited by 2
CategoryTheory.Presieve.isSheafFor_singleton_isoproof · cited by 1
CategoryTheory.Types.singleton_mem_jointlySurjectivePrecoverage_iffproof · cited by 0
CategoryTheory.Presieve.singleton_eq_iff_domainproof · cited by 0
CategoryTheory.Presieve.uncurry_singletonproof · cited by 0
CategoryTheory.Functor.isCoverDense_of_generate_singleton_functor_π_memproof · cited by 0
CategoryTheory.Presieve.pullback_singletonproof · cited by 0
CategoryTheory.Presieve.FamilyOfElements.compatible_singleton_iffproof · cited by 0
CategoryTheory.Presieve.FamilyOfElements.isAmalgamation_singleton_iffproof · cited by 0