Theorems · Definition · category theory
CategoryTheory.MorphismProperty.ofHoms.casesOn
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type u_3} {X Y : ι → C} {f : (i : ι) → X i ⟶ Y i}
{motive : ⦃X_1 Y_1 : C⦄ → (x : X_1 ⟶ Y_1) → CategoryTheory.MorphismProperty.ofHoms f x → Prop} ⦃X_1 Y_1 : C⦄
{x : X_1 ⟶ Y_1} (t : CategoryTheory.MorphismProperty.ofHoms f x), (∀ (i : ι), motive (f i) ⋯) → motive x t- Cited by
- 26 results in Mathlib
- Foundations
- Depth 6 from the axioms · uses no axioms
- Assumes
- CategoryTheory.Category
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.MorphismProperty.ofHomsstatement and proof · cited by 30
Cited by26
Results whose statement or proof uses this declaration.
- CategoryTheory.MorphismProperty.ofHoms_iffproof · cited by 8
- CategoryTheory.SmallObject.SuccStruct.prop.facproof · cited by 2
- CategoryTheory.SmallObject.SuccStruct.prop.succ_eqproof · cited by 2
- SSet.Subcomplex.Pairing.anodyneExtensionsproof · cited by 2
- SSet.Subcomplex.Pairing.innerAnodyneExtensionsproof · cited by 2
- HomotopicalAlgebra.ReedyStructure.prop₁_of_degHom_eq_deg_rightproof · cited by 2
- SSet.innerFibration_pullbackObjObjπproof · cited by 1
- CategoryTheory.SmallObject.SuccStruct.prop_iffproof · cited by 1
- CategoryTheory.MorphismProperty.isLocal_single_iff_bijectiveproof · cited by 1
- CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.eq_id_of_D₂_Wproof · cited by 1