Basic

📁 Source: Mathlib/Geometry/Manifold/Sheaf/Basic.lean

Statistics

Metric	Count
Definitions localPredicate, sheaf, sheafHasCoeToFun, chartedSpace	4
Theorems section_spec, hasGroupoid	2
Total	6

StructureGroupoid.LocalInvariantProp

Definitions

Name	Category	Theorems
localPredicate 📖	CompOp	5 math math: smoothSheafCommRing.eval_germ, smoothSheafCommRing.evalHom_germ, section_spec, smoothSheaf.eval_germ, smoothSheaf.contMDiff_section
sheaf 📖	CompOp	—
sheafHasCoeToFun 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
section_spec 📖	mathematical	StructureGroupoid.LocalInvariantProp	ChartedSpace.LiftProp TopCat.carrier TopCat.of TopologicalSpace.Opens TopCat.str SetLike.instMembership TopologicalSpace.Opens.instSetLike Opposite.unop instTopologicalSpaceSubtype TopologicalSpace.Opens.instChartedSpace TopCat.PrelocalPredicate.pred TopCat.LocalPredicate.toPrelocalPredicate localPredicate	—	—

TopCat.of

Definitions

Name	Category	Theorems
chartedSpace 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasGroupoid 📖	mathematical	—	HasGroupoid TopCat.carrier TopCat.of	—	—

---

← Back to Index