Theorems · Definition · category theory

HomotopicalAlgebra.Cylinder.IsGood.casesOn

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : C} →
      [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C] →
        {P : HomotopicalAlgebra.Cylinder A} →
          [inst_2 : CategoryTheory.Limits.HasBinaryCoproduct A A] →
            [inst_3 : HomotopicalAlgebra.CategoryWithCofibrations C] →
              {motive : P.IsGood → Sort u_1} →
                (t : P.IsGood) → ((cofibration_i : HomotopicalAlgebra.Cofibration P.i) → motive ⋯) → motive t

Defined in: Mathlib.AlgebraicTopology.ModelCategory.Cylinder
Cited by: 0 results in Mathlib
Foundations: Depth 28 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CategoryTheory.Category HomotopicalAlgebra.CategoryWithWeakEquivalences CategoryTheory.Limits.HasBinaryCoproduct HomotopicalAlgebra.CategoryWithCofibrations

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites11

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
CategoryTheory.Limits.coprodstatement · cited by 252
CategoryTheory.Limits.HasBinaryCoproductstatement and proof · cited by 81
HomotopicalAlgebra.CategoryWithWeakEquivalencesstatement and proof · cited by 77
HomotopicalAlgebra.Precylinder.Istatement · cited by 75
HomotopicalAlgebra.CategoryWithCofibrationsstatement and proof · cited by 46
HomotopicalAlgebra.Cylinderstatement and proof · cited by 31
HomotopicalAlgebra.Cofibrationstatement and proof · cited by 27
HomotopicalAlgebra.Cylinder.toPrecylinderstatement and proof · cited by 23
HomotopicalAlgebra.Precylinder.istatement and proof · cited by 13
HomotopicalAlgebra.Cylinder.IsGoodstatement and proof · cited by 11

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.