Theorems · Theorem · category theory
TopCat.subpresheafToTypes.isSheaf
∀ {X : TopCat} {T : ↑X → Type u_1} (P : TopCat.LocalPredicate T),
(TopCat.subpresheafToTypes P.toPrelocalPredicate).IsSheafThe functions satisfying a local predicate satisfy the sheaf condition.
- Defined in
- Mathlib.Topology.Sheaves.LocalPredicate
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 90 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites24
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- CategoryTheory.Functor.objproof · cited by 19,642
- TopCat.carrierstatement and proof · cited by 3,184
- iSupproof · cited by 2,415
- Opposite.unopproof · cited by 2,231
- TopologicalSpace.Opensproof · cited by 2,040
- TopCatstatement and proof · cited by 1,889
- CategoryTheory.ObjectProperty.FullSubcategory.objproof · cited by 1,316
- CategoryTheory.ToTypeproof · cited by 219
- TopCat.PrelocalPredicate.predproof · cited by 56
- TopCat.LocalPredicate.toPrelocalPredicatestatement and proof · cited by 48
- TopCat.Presheaf.IsSheafstatement · cited by 38
Cited by1
Results whose statement or proof uses this declaration.
- TopCat.subsheafToTypesproof · cited by 5