Theorems · Definition · category theory
CategoryTheory.Functor.PreOneHypercoverDenseData.X
{C₀ : Type u₀} →
{C : Type u} →
[inst : CategoryTheory.Category.{v₀, u₀} C₀] →
[inst_1 : CategoryTheory.Category.{v, u} C] →
{F : CategoryTheory.Functor C₀ C} → {S : C} → (self : F.PreOneHypercoverDenseData S) → self.I₀ → C₀the objects in the covering of S
- Cited by
- 44 results in Mathlib
- Foundations
- Depth 4 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
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.Functorstatement and proof · cited by 16,252
- CategoryTheory.Functor.PreOneHypercoverDenseData.I₀statement · cited by 45
- CategoryTheory.Functor.PreOneHypercoverDenseDatastatement and proof · cited by 27
Cited by63
Results whose statement or proof uses this declaration.
- CategoryTheory.Functor.PreOneHypercoverDenseData.fstatement · cited by 33
- CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjπstatement · cited by 23
- CategoryTheory.Functor.PreOneHypercoverDenseData.toPreOneHypercoverproof · cited by 17
- CategoryTheory.Functor.PreOneHypercoverDenseData.multicospanIndexproof · cited by 11
- CategoryTheory.Functor.PreOneHypercoverDenseData.p₁statement · cited by 10
- CategoryTheory.Functor.PreOneHypercoverDenseData.p₂statement · cited by 10
- CategoryTheory.Functor.PreOneHypercoverDenseData.sieve₁₀statement and proof · cited by 8
- CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafMap_πstatement · cited by 5
- CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObj_hom_extstatement · cited by 5
- CategoryTheory.Functor.OneHypercoverDenseData.SieveStruct.qstatement · cited by 4
- CategoryTheory.Functor.OneHypercoverDenseData.SieveStruct.facstatement · cited by 3
- CategoryTheory.Functor.OneHypercoverDenseData.mem₁₀statement · cited by 3