Theorems · Inductive type · global analysis
DiffeologicalSpace
Type u_1 → Type u_1
A diffeology on X, given by the smooth functions (or "plots") from ℝⁿ to X.
- Defined in
- Mathlib.Geometry.Diffeology.Basic
- Cited by
- 60 results in Mathlib
- Foundations
- Depth 0 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites0
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Nothing in Mathlib beyond the foundations.
Cited by84
Results whose statement or proof uses this declaration.
- Diffeology.IsPlotstatement and proof · cited by 29
- DiffeologicalSpace.generateFromstatement and proof · cited by 18
- DiffeologicalSpace.toPlotsstatement and proof · cited by 18
- Diffeology.DSmoothstatement and proof · cited by 16
- DiffeologicalSpace.giGenerateFromstatement · cited by 8
- Diffeology.IsContDiffCompatiblestatement · cited by 8
- DiffeologicalSpace.gc_generateFromstatement · cited by 6
- DiffeologicalSpace.plotsstatement and proof · cited by 5
- Diffeology.dTopologystatement · cited by 5
- DiffeologicalSpace.extstatement and proof · cited by 4
- DiffeologicalSpace.dTopologystatement and proof · cited by 2
- DiffeologicalSpace.generateFrom_le_iff_subset_toPlotsstatement and proof · cited by 2