LocallySurjective

📁 Source: Mathlib/Topology/Sheaves/LocallySurjective.lean

Statistics

Metric	Count
Definitions IsLocallySurjective	1
Theorems isLocallySurjective_iff, locally_surjective_iff_surjective_on_stalks	2
Total	3

TopCat.Presheaf

Definitions

Name	Category	Theorems
IsLocallySurjective 📖	MathDef	2 math math: locally_surjective_iff_surjective_on_stalks, isLocallySurjective_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isLocallySurjective_iff 📖	mathematical	—	IsLocallySurjective DFunLike.coe CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Opposite.op CategoryTheory.ConcreteCategory.hom CategoryTheory.NatTrans.app restrict SetLike.instMembership TopologicalSpace.Opens.instSetLike	—	CategoryTheory.Presheaf.IsLocallySurjective.imageSieve_mem
locally_surjective_iff_surjective_on_stalks 📖	mathematical	—	IsLocallySurjective CategoryTheory.Functor.obj TopCat.Presheaf TopCat.instCategoryPresheaf stalkFunctor DFunLike.coe CategoryTheory.ConcreteCategory.hom CategoryTheory.Functor.map	—	germ_exist CategoryTheory.Presheaf.IsLocallySurjective.imageSieve_mem stalkFunctor_map_germ_apply' germ_res_apply germ_eq stalkFunctor_map_germ_apply CategoryTheory.NatTrans.naturality

---

← Back to Index