Theorems · Definition · category theory

CategoryTheory.Pairwise.casesOn

{ι : Type v} →
  {motive : CategoryTheory.Pairwise ι → Sort u} →
    (t : CategoryTheory.Pairwise ι) →
      ((a : ι) → motive (CategoryTheory.Pairwise.single a)) →
        ((a a_1 : ι) → motive (CategoryTheory.Pairwise.pair a a_1)) → motive t

Defined in: Mathlib.CategoryTheory.Category.Pairwise
Cited by: 6 results in Mathlib
Foundations: Depth 3 from the axioms · uses no axioms

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites1

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

CategoryTheory.Pairwisestatement and proof · cited by 40

Cited by13

Results whose statement or proof uses this declaration.

TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverseObjproof · cited by 3
TopCat.Presheaf.isSheaf_iff_isSheafUniqueGluing_typesproof · cited by 2
TopCat.Sheaf.interUnionPullbackConeLiftproof · cited by 2
AlgebraicGeometry.isIso_pushoutSection_of_iSup_eqproof · cited by 2
CategoryTheory.Pairwise.ctorElimproof · cited by 0
CategoryTheory.Pairwise.ctorIdxproof · cited by 0
TopCat.Sheaf.interUnionPullbackConeLift_leftproof · cited by 0
TopCat.Presheaf.isGluing_iff_pairwiseproof · cited by 0
TopCat.Sheaf.interUnionPullbackConeLift_rightproof · cited by 0
TopCat.Presheaf.SheafCondition.pairwiseDiagramIsoproof · cited by 0
CategoryTheory.Pairwise.noConfusionproof · cited by 0
TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverseObj_π_appstatement · cited by 0