Theorems · Definition · category theory
TopCat.subsheafToTypes
{X : TopCat} → {T : ↑X → Type u_1} → TopCat.LocalPredicate T → TopCat.Sheaf (Type (max u_2 u_1)) XThe subsheaf of the sheaf of all dependently typed functions satisfying the local predicate P.
- Defined in
- Mathlib.Topology.Sheaves.LocalPredicate
- Cited by
- 5 results in Mathlib
- Foundations
- Depth 91 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- TopCat.carrierstatement and proof · cited by 3,184
- TopCatstatement and proof · cited by 1,889
- TopCat.Sheafstatement · cited by 73
- TopCat.LocalPredicate.toPrelocalPredicateproof · cited by 48
- TopCat.LocalPredicatestatement and proof · cited by 10
- TopCat.subpresheafToTypesproof · cited by 6
- TopCat.subpresheafToTypes.isSheafproof · cited by 0
Cited by10
Results whose statement or proof uses this declaration.
- AlgebraicGeometry.structureSheafInTypeproof · cited by 59
- TopCat.stalkToFiberstatement · cited by 4
- TopCat.Presheaf.sheafifyproof · cited by 2
- AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.structureSheafInTypeproof · cited by 2
- TopCat.stalkToFiber_germstatement and proof · cited by 2
- TopCat.stalkToFiber_surjectivestatement and proof · cited by 2
- TopCat.stalkToFiber_ιstatement · cited by 1
- StructureGroupoid.LocalInvariantProp.sheafproof · cited by 1
- TopCat.stalkToFiber_injectivestatement and proof · cited by 1
- TopCat.subsheafToTypes_objstatement and proof · cited by 0