Theorems · Definition · category theory
SimplexCategoryGenRel.faces.casesOn
∀ {motive : ⦃X Y : SimplexCategoryGenRel⦄ → (x : X ⟶ Y) → SimplexCategoryGenRel.faces x → Prop}
⦃X Y : SimplexCategoryGenRel⦄ {x : X ⟶ Y} (t : SimplexCategoryGenRel.faces x),
(∀ {n : ℕ} (i : Fin (n + 2)), motive (SimplexCategoryGenRel.δ i) ⋯) → motive x t- Cited by
- 5 results in Mathlib
- Foundations
- Depth 22 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Quiver.Homstatement and proof · cited by 32,603
- SimplexCategoryGenRelstatement and proof · cited by 39
- SimplexCategoryGenRel.mkstatement and proof · cited by 39
- SimplexCategoryGenRel.δstatement and proof · cited by 20
- SimplexCategoryGenRel.facesstatement and proof · cited by 5
Cited by5
Results whose statement or proof uses this declaration.
- SimplexCategoryGenRel.hom_inductionproof · cited by 1
- SimplexCategoryGenRel.eq_or_len_le_of_P_δproof · cited by 0
- SimplexCategoryGenRel.exists_P_σ_P_δ_factorizationproof · cited by 0
- SimplexCategoryGenRel.isSplitMono_P_δproof · cited by 0
- SimplexCategoryGenRel.hom_induction'proof · cited by 0