Theorems · Definition · global analysis
smoothPresheafAddGroup
{𝕜 : Type u_1} →
[inst : NontriviallyNormedField 𝕜] →
{EM : Type u_2} →
[inst_1 : NormedAddCommGroup EM] →
[inst_2 : NormedSpace 𝕜 EM] →
{HM : Type u_3} →
[inst_3 : TopologicalSpace HM] →
ModelWithCorners 𝕜 EM HM →
{E : Type u_4} →
[inst_4 : NormedAddCommGroup E] →
[inst_5 : NormedSpace 𝕜 E] →
{H : Type u_5} →
[inst_6 : TopologicalSpace H] →
(I : ModelWithCorners 𝕜 E H) →
(M : Type u) →
[inst_7 : TopologicalSpace M] →
[ChartedSpace HM M] →
(G : Type u) →
[inst_9 : TopologicalSpace G] →
[inst_10 : ChartedSpace H G] →
[inst_11 : AddGroup G] →
[LieAddGroup I (↑⊤) G] → TopCat.Presheaf AddGrpCat (TopCat.of M)The presheaf of smooth functions from M to G, for G an additive Lie group,
as a presheaf of additive groups.
- Defined in
- Mathlib.Geometry.Manifold.Sheaf.Smooth
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 217 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites23
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Quiver.Homproof · cited by 32,603
- TopologicalSpacestatement and proof · cited by 24,529
- CategoryTheory.Functor.objproof · cited by 19,642
- NormedAddCommGroupstatement and proof · cited by 15,752
- NormedSpacestatement and proof · cited by 12,499
- Top.topstatement and proof · cited by 9,680
- NontriviallyNormedFieldstatement and proof · cited by 8,742
- Oppositeproof · cited by 8,081
- ENatstatement · cited by 4,985
- AddGroupstatement and proof · cited by 4,410
- TopCat.carrierproof · cited by 3,184
- ModelWithCornersstatement and proof · cited by 2,462
Cited by1
Results whose statement or proof uses this declaration.
- smoothSheafAddGroupproof · cited by 0