Structures · Geometry
DiffeologicalSpace
A diffeology on X, given by the smooth functions (or "plots") from ℝⁿ to X.
- Defined in
- Mathlib.Geometry.Diffeology.Basic
- Shape
- One type argument · adds plots, constant_plots, plot_reparam, locality, dTopology, isOpen_iff_preimages_plots
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances2
- Real
- EuclideanSpace
How is a type an instance?
Loading the hierarchy index…
Assumed by33
- Diffeology.IsPlot
- Diffeology.DSmooth
- Diffeology.dTopology
- DiffeologicalSpace.plots
- ContDiff.isPlot
- Diffeology.isOpen_iff_preimages_plots
- Diffeology.isPlot_iff_contDiff
- DiffeologicalSpace.dTopology
- Diffeology.IsPlot.contDiff
- Diffeology.DSmooth.contDiff
- Diffeology.isPlot_const
- Diffeology.DSmooth.comp
- Diffeology.DSmooth.isPlot
- ContDiff.dSmooth
- Diffeology.dSmooth_id
- DiffeologicalSpace.isOpen_iff_preimages_plots
- Diffeology.DSmooth.continuous
- Diffeology.isPlot_reparam
- DiffeologicalSpace.plot_reparam
- Diffeology.IsPlot.dSmooth
- DiffeologicalSpace.constant_plots
- DiffeologicalSpace.locality
- Diffeology.DSmooth.continuous'
- Diffeology.dSmooth_iff_contDiff
- Diffeology.IsPlot.dSmooth_comp'
- Diffeology.isPlot_iff_dSmooth
- Diffeology.dSmooth_iff
- Diffeology.DSmooth.comp'
- Diffeology.dSmooth_const
- Diffeology.IsPlot.continuous
- NormedSpace.isContDiffCompatible_iff_eq_toDiffeology
- Diffeology.dSmooth_id'
- Diffeology.IsPlot.dSmooth_comp
Ancestors0
No ancestors.