Diffeological spaces

A diffeological space is a concrete sheaf on the site of cartesian spaces ℝⁿ and smooth maps between them, or equivalently a type X with a well-behaved notion of smoothness for functions from the spaces ℝⁿ to X - see https://ncatlab.org/nlab/show/diffeological+space. In this file we focus on the latter viewpoint and define some of the basic notions of diffeology, like diffeological spaces and smooth maps between them.

Concretely, this means that for our purposes a diffeological space is a type X together with a set plots n of maps ℝⁿ → X for each n (called plots), such that the following three properties hold:

• Every constant map is a plot.
• For every plot p : ℝⁿ → X and smooth map f : ℝᵐ → ℝⁿ, p ∘ f is a plot.
• Every map p : ℝⁿ → X that is locally smooth is a plot, where by locally smooth we mean that ℝⁿ can be covered by open sets U such that p ∘ f is a plot for every smooth f : ℝᵐ → U. Every normed space, smooth manifold etc. is then naturally a diffeological space by simply taking the plots to be those maps ℝⁿ → X that are smooth in the traditional sense. A map f : X → Y between diffeological spaces is furthermore called smooth if postcomposition with it sends plots of X to plots of Y. This is equivalent to the usual definition of smoothness for maps between e.g. manifolds, and equivalent to being a plot for maps p : ℝⁿ → X.

In addition to this notion of smoothness, every diffeological space X also comes equipped with a natural diffeology, called the D-topology; it is the finest topology on X that makes all plots continuous, and consists precisely of those sets whose preimages under plots are all open. This recovers the standard topology of e.g. normed spaces and manifolds, and makes all smooth maps continuous. We provide this as a definition but not as an instance, for reasons outlined in the implementation details below.

Main definitions / results

• DiffeologicalSpace X: the type of diffeologies on a type X.
• IsPlot p: predicate stating that a map p : ℝⁿ → X is a plot, i.e. belongs to the diffeology on X.
• DSmooth f: predicate stating that a map f : X → Y between diffeological spaces is smooth in the sense that it sends plots to plots. This is the correct notion of morphisms between diffeological spaces.
• dTopology: the D-topology on a diffeological space, consisting of all sets U whose preimage p ⁻¹' u is open for all plots p. This is a definition rather than an instance to avoid typeclass diamonds (see below), and meant for use with notation such as Continuous[_, dTopology].
• IsDTopologyCompatible X: typeclass stating that X is equipped with a topology that is equal (but not necessarily defeq) to the D-topology.
• NormedSpace.toDiffeology: the standard diffeology on any finite-dimensional normed space X, consisting of all conventionally smooth maps ℝⁿ → X. This is again a definition rather than a instance for typeclass diamond reasons; however, we do put this as an instance on ℝ and EuclideanSpace ℝ ι for finite ι.
• IsContDiffCompatible X: typeclass stating that the diffeology on a normed space X is equal to the diffeology whose plots are precisely the smooth maps.
• isPlot_iff_dSmooth: a map ℝⁿ → X is a plot iff it is smooth.
• dSmooth_iff_contDiff: a map between finite-dimensional normed spaces is smooth in the sense of DSmooth iff it is smooth in the sense of ContDiff ℝ ∞.

Implementation notes

Choice of test spaces

Instead of defining diffeologies as collections of plots ℝⁿ → X whose domains are the spaces ℝⁿ, we could have also defined them in terms of maps from some other collection of test spaces; for example:

• all open balls in the spaces ℝⁿ
• all open subsets of the spaces ℝⁿ
• all finite-dimensional normed spaces, or open balls therein / open subsets thereof
• all finite-dimensional smooth manifolds.

All of these result in equivalent notions of diffeologies and smooth maps; the abstract way to see this is that the corresponding sites are all dense subsites of the site of finite-dimensional smooth manifolds, and hence give rise to equivalent sheaf topoi. Which of those sites / collections of test spaces to use is hence mainly a matter of convenience; we have gone with the cartesian spaces ℝⁿ mainly for two reasons:

• They are the simplest to work with for practical purposes: maps between subsets are more annoying to deal with formally than maps between types, and e.g. smooth manifolds are extremely annoying to quantify over, while the cartesian spaces ℝⁿ are indexed simply by the natural numbers ℕ.
• Working with e.g. all finite-dimensional normed spaces instead of this particular choice of representatives would lead to an unnecessary universe bump.

One downside of this choice compared to that of all open subsets of ℝⁿ is however that it makes the sheaf condition / locality condition of diffeologies ("any map that is locally a plot is also globally a plot") somewhat awkward to state and prove. To mitigate this, we provide DiffeologicalSpace.ofPlotsOn as a way to construct a diffeology from plots whose domains are subsets of ℝⁿ. See the definition of NormedSpace.toDiffeology for an example where this is used.

D-Topology

While the D-topology is quite well-behaved in some regards, it does unfortunately not always commute with e.g. products. This means that it can not be registered as an instance - otherwise, there would be two TopologicalSpace-instances on binary products, the product topology of the D-topologies on the factors and the D-topology of the product diffeology. For emphasis we repeat: in general these topologies can be mathematically distinct not just non-defeq. We thus instead define a typeclass IsDTopologyCompatible X to express when the topology on X does match the D-topology, and also give the D-topology the short name dTopology to enable use of notations such as Continuous[_, dTopology] for continuity with respect to the D-topology.

In order to make it easier to work with diffeological spaces whose natural diffeology does match the D-topology, we also include the D-topology as part of the data of DiffeologicalSpace X. This allows the diffeologies on e.g. ℝⁿ, manifolds and quotients of diffeological spaces to be defined in such a way that the D-topology is defeq to the topology that the space already carries.

Diffeologies on normed spaces

Every normed spaces carries a natural diffeology consisting of all smooth maps from ℝⁿ. While this "normed space diffeology" does commute with arbitrary products, we can't register it as an instance because it wouldn't be defeq to the product diffeology on products of normed spaces. We thus only give it as a definition (NormedSpace.toDiffeology) instead of an instance, and instead provide a typeclass IsContDiffCompatible X for talking about normed spaces equipped with the normed space diffeology.

To make working with finite-dimensional spaces easier, NormedSpace.toDiffeology is defined in such a way that its D-topology is defeq to the topology induced by the norm - however, this currently comes at the cost of making the definition work only on finite-dimensional spaces. It should be possible to extend this to all normed spaces though in the future.

TODO

Much of the basic theory of diffeological spaces has already been formalised at https://github.com/peabrainiac/lean-orbifolds and just needs to be upstreamed. However, some TODOs that haven't been formalised at all yet and only depend on the material here are:

• Generalise NormedSpace.toDiffeology to infinite-dimensional normed spaces. The hard part of this is showing that the D-topology of any normed space is just its usual topology, as is needed to make that equality definitional. On paper, this is relatively straightforward: for a set U ⊆ X that is not open under the standard normed space topology, take a sequence x_i outside of U that converges to a point in U, a smooth map ℝ → X under which a convergent sequence in ℝ maps to this sequence (x_i), and use it to conclude that U is not D-open either. However, constructing the needed smooth map explicitly is probably a lot of work.
• Generalise dSmooth_iff_contDiff to infinite-dimensional normed spaces if possible. There should be some references at least for the case of Banach spaces in the literature.

References

• Patrick Iglesias-Zemmour, Diffeology
• https://ncatlab.org/nlab/show/diffeological+space

Tags

diffeology, diffeological space, smoothness, smooth function

class DiffeologicalSpace (X : Type u_1) : Type u_1

A diffeology on X, given by the smooth functions (or "plots") from ℝⁿ to X.

• plots (n : ℕ) : Set (EuclideanSpace ℝ (Fin n) → X)

  The plots EuclideanSpace ℝ (Fin n) → X representing the smooth ways to map EuclideanSpace ℝ (Fin n) into X. This is the main piece of data underlying the diffeology.

• constant_plots {n : ℕ} (x : X) : (fun (x_1 : EuclideanSpace ℝ (Fin n)) => x) ∈ plots n

  Every constant map needs to be a plot.

• plot_reparam {n m : ℕ} {p : EuclideanSpace ℝ (Fin m) → X} {f : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin m)} (hp : p ∈ plots m) (hf : ContDiff ℝ (↑⊤) f) : p ∘ f ∈ plots n

  Smooth reparametrisations of plots need to be plots.

• locality {n : ℕ} {p : EuclideanSpace ℝ (Fin n) → X} (hp : ∀ (x : EuclideanSpace ℝ (Fin n)), ∃ (u : Set (EuclideanSpace ℝ (Fin n))), IsOpen u ∧ x ∈ u ∧ ∀ {m : ℕ} {f : EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin n)}, (∀ (x : EuclideanSpace ℝ (Fin m)), f x ∈ u) → ContDiff ℝ (↑⊤) f → p ∘ f ∈ plots m) : p ∈ plots n

  Every locally smooth map EuclideanSpace ℝ (Fin n) → X is a plot.

• dTopology : TopologicalSpace X

  The D-topology of the diffeology. This is included as part of the data in order to give control over what the D-topology is defeq to. See also note [forgetful inheritance].

• isOpen_iff_preimages_plots {u : Set X} : TopologicalSpace.IsOpen u ↔ ∀ {n : ℕ}, ∀ p ∈ plots n, IsOpen (p ⁻¹' u)

  The D-topology consists of exactly those sets whose preimages under plots are all open.

def Diffeology.dTopology {X : Type u_1} [self : DiffeologicalSpace X] : TopologicalSpace X

Alias of DiffeologicalSpace.dTopology.

---

The D-topology of the diffeology. This is included as part of the data in order to give control over what the D-topology is defeq to. See also note [forgetful inheritance].

Equations

• @Diffeology.dTopology = @DiffeologicalSpace.dTopology

def Diffeology.IsPlot {X : Type u_1} [DiffeologicalSpace X] {n : ℕ} (p : EuclideanSpace ℝ (Fin n) → X) : Prop

A map p : EuclideanSpace ℝ (Fin n) → X is called a plot iff it is part of the diffeology on X. This is equivalent to p being smooth with respect to the standard diffeology on EuclideanSpace ℝ (Fin n).

Equations

• Diffeology.IsPlot p = (p ∈ DiffeologicalSpace.plots n)

def Diffeology.DSmooth {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] (f : X → Y) : Prop

A function between diffeological spaces is smooth iff composition with it preserves smoothness of plots.

Equations

• Diffeology.DSmooth f = ∀ (n : ℕ) (p : EuclideanSpace ℝ (Fin n) → X), Diffeology.IsPlot p → Diffeology.IsPlot (f ∘ p)

theorem DiffeologicalSpace.ext {X : Type u_4} {d₁ d₂ : DiffeologicalSpace X} (h : @Diffeology.IsPlot X d₁ = @Diffeology.IsPlot X d₂) : d₁ = d₂

theorem DiffeologicalSpace.ext_iff {X : Type u_4} {d₁ d₂ : DiffeologicalSpace X} : d₁ = d₂ ↔ @Diffeology.IsPlot X d₁ = @Diffeology.IsPlot X d₂

theorem Diffeology.isPlot_const {X : Type u_1} [DiffeologicalSpace X] {n : ℕ} {x : X} : IsPlot fun (x_1 : EuclideanSpace ℝ (Fin n)) => x

theorem Diffeology.isPlot_reparam {X : Type u_1} [DiffeologicalSpace X] {n m : ℕ} {p : EuclideanSpace ℝ (Fin m) → X} {f : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin m)} (hp : IsPlot p) (hf : ContDiff ℝ (↑⊤) f) : IsPlot (p ∘ f)

theorem Diffeology.IsPlot.dSmooth_comp {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] {n : ℕ} {p : EuclideanSpace ℝ (Fin n) → X} {f : X → Y} (hp : IsPlot p) (hf : DSmooth f) : IsPlot (f ∘ p)

theorem Diffeology.IsPlot.dSmooth_comp' {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] {n : ℕ} {p : EuclideanSpace ℝ (Fin n) → X} {f : X → Y} (hp : IsPlot p) (hf : DSmooth f) : IsPlot fun (x : EuclideanSpace ℝ (Fin n)) => f (p x)

theorem Diffeology.isOpen_iff_preimages_plots {X : Type u_1} [DiffeologicalSpace X] {u : Set X} : IsOpen u ↔ ∀ (n : ℕ) (p : EuclideanSpace ℝ (Fin n) → X), IsPlot p → IsOpen (p ⁻¹' u)

theorem Diffeology.IsPlot.continuous {X : Type u_1} [DiffeologicalSpace X] {n : ℕ} {p : EuclideanSpace ℝ (Fin n) → X} (hp : IsPlot p) : Continuous p

theorem Diffeology.DSmooth.continuous {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] {f : X → Y} (hf : DSmooth f) : Continuous f

theorem Diffeology.dSmooth_iff {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] {f : X → Y} : DSmooth f ↔ ∀ (n : ℕ) (p : EuclideanSpace ℝ (Fin n) → X), IsPlot p → IsPlot (f ∘ p)

theorem Diffeology.dSmooth_id {X : Type u_1} [DiffeologicalSpace X] : DSmooth id

theorem Diffeology.dSmooth_id' {X : Type u_1} [DiffeologicalSpace X] : DSmooth fun (x : X) => x

theorem Diffeology.DSmooth.comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace Y] [DiffeologicalSpace Z] {f : X → Y} {g : Y → Z} (hg : DSmooth g) (hf : DSmooth f) : DSmooth (g ∘ f)

theorem Diffeology.DSmooth.comp' {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace Y] [DiffeologicalSpace Z] {f : X → Y} {g : Y → Z} (hg : DSmooth g) (hf : DSmooth f) : DSmooth fun (x : X) => g (f x)

theorem Diffeology.dSmooth_const {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] {y : Y} : DSmooth fun (x : X) => y

def DiffeologicalSpace.replaceDTopology {X : Type u_1} (d : DiffeologicalSpace X) (t : TopologicalSpace X) (h : dTopology = t) : DiffeologicalSpace X

Replaces the D-topology of a diffeology with another topology equal to it. Useful to construct diffeologies with better definitional equalities.

Equations

• d.replaceDTopology t h = { plots := DiffeologicalSpace.plots, constant_plots := ⋯, plot_reparam := ⋯, locality := ⋯, dTopology := t, isOpen_iff_preimages_plots := ⋯ }

theorem DiffeologicalSpace.replaceDTopology_eq {X : Type u_1} {d : DiffeologicalSpace X} {t : TopologicalSpace X} {h : dTopology = t} : d.replaceDTopology t h = d

structure DiffeologicalSpace.CorePlotsOn (X : Type u_1) : Type u_1

A structure with plots specified on open subsets of ℝⁿ rather than ℝⁿ itself. Useful for constructing diffeologies, as it often makes the locality condition easier to prove.

• isPlotOn {n : ℕ} {u : Set (EuclideanSpace ℝ (Fin n))} (hu : IsOpen u) : (EuclideanSpace ℝ (Fin n) → X) → Prop

  The predicate determining which maps u → X with u : Set (EuclideanSpace ℝ (Fin n)) open are plots.

• isPlotOn_congr {n : ℕ} {u : Set (EuclideanSpace ℝ (Fin n))} (hu : IsOpen u) {p q : EuclideanSpace ℝ (Fin n) → X} (h : Set.EqOn p q u) : self.isPlotOn hu p ↔ self.isPlotOn hu q
• isPlot {n : ℕ} : (EuclideanSpace ℝ (Fin n) → X) → Prop

  The predicate that the diffeology built from this structure will use. Can be overwritten to allow for better definitional equalities.

• isPlotOn_univ {n : ℕ} {p : EuclideanSpace ℝ (Fin n) → X} : self.isPlotOn ⋯ p ↔ self.isPlot p
• isPlot_const {n : ℕ} (x : X) : self.isPlot fun (x_1 : EuclideanSpace ℝ (Fin n)) => x
• isPlotOn_reparam {n m : ℕ} {u : Set (EuclideanSpace ℝ (Fin n))} {v : Set (EuclideanSpace ℝ (Fin m))} {hu : IsOpen u} (hv : IsOpen v) {p : EuclideanSpace ℝ (Fin n) → X} {f : EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin n)} (h : Set.MapsTo f v u) (hp : self.isPlotOn hu p) (hf : ContDiffOn ℝ (↑⊤) f v) : self.isPlotOn hv (p ∘ f)
• locality {n : ℕ} {u : Set (EuclideanSpace ℝ (Fin n))} (hu : IsOpen u) {p : EuclideanSpace ℝ (Fin n) → X} (hp : ∀ x ∈ u, ∃ (v : Set (EuclideanSpace ℝ (Fin n))) (hv : IsOpen v), x ∈ v ∧ self.isPlotOn hv p) : self.isPlotOn hu p

  The locality axiom of diffeologies, phrased in terms of isPlotOn.

• dTopology : TopologicalSpace X

  The D-topology that the diffeology built from this structure will use. Can be overwritten to allow for better definitional equalities.

• isOpen_iff_preimages_plots {u : Set X} : TopologicalSpace.IsOpen u ↔ ∀ {n : ℕ} (p : EuclideanSpace ℝ (Fin n) → X), self.isPlot p → IsOpen (p ⁻¹' u)

def DiffeologicalSpace.ofCorePlotsOn {X : Type u_1} (d : CorePlotsOn X) : DiffeologicalSpace X

Constructs a diffeology from plots defined on open subsets or ℝⁿ rather than ℝⁿ itself, organised in the form of the auxiliary CorePlotsOn structure. This is more involved in most regards, but also often makes it quite a lot easier to prove the locality condition.

Equations

• One or more equations did not get rendered due to their size.

class Diffeology.IsDTopologyCompatible (X : Type u_1) [t : TopologicalSpace X] [DiffeologicalSpace X] : Prop

Technical condition saying that the topology on a type agrees with the D-topology. Necessary because the D-topologies on for example products and subspaces don't agree with the product and subspace topologies.

• dTop_eq : dTopology = t

theorem Diffeology.DSmooth.continuous' {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [DiffeologicalSpace X] [IsDTopologyCompatible X] [TopologicalSpace Y] [DiffeologicalSpace Y] [IsDTopologyCompatible Y] {f : X → Y} (hf : DSmooth f) : Continuous f

A smooth function between spaces that are equipped with the D-topology is continuous.

class Diffeology.IsContDiffCompatible (X : Type u_1) [NormedAddCommGroup X] [NormedSpace ℝ X] [DiffeologicalSpace X] : Prop

Technical condition saying that the diffeology on a space is the one coming from smoothness in the sense of ContDiff ℝ ∞. Necessary as a hypothesis for some theorems because some normed spaces carry a diffeology that is equal but not defeq to the normed space diffeology (for example the product diffeology in the case of Fin n → ℝ), so the information that these theorems still holds needs to be made available via this typeclass.

• isPlot_iff {n : ℕ} {p : EuclideanSpace ℝ (Fin n) → X} : IsPlot p ↔ ContDiff ℝ (↑⊤) p

def NormedSpace.toDiffeology (X : Type u_1) [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] : DiffeologicalSpace X

Diffeology on a finite-dimensional normed space. We make this a definition instead of an instance because we also want to have product diffeologies as an instance, and having both would cause instance diamonds on spaces like Fin n → ℝ.

Equations

• One or more equations did not get rendered due to their size.

instance Diffeology.instIsContDiffCompatible {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] : IsContDiffCompatible X

theorem NormedSpace.isContDiffCompatible_iff_eq_toDiffeology {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] [d : DiffeologicalSpace X] : Diffeology.IsContDiffCompatible X ↔ d = toDiffeology X

instance Diffeology.instIsDTopologyCompatible {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] : IsDTopologyCompatible X

instance Diffeology.instDiffeologicalSpaceReal : DiffeologicalSpace ℝ

Equations

• Diffeology.instDiffeologicalSpaceReal = NormedSpace.toDiffeology ℝ

instance Diffeology.instDiffeologicalSpaceEuclideanSpaceRealOfFintype {ι : Type u_1} [Fintype ι] : DiffeologicalSpace (EuclideanSpace ℝ ι)

Equations

• Diffeology.instDiffeologicalSpaceEuclideanSpaceRealOfFintype = NormedSpace.toDiffeology (EuclideanSpace ℝ ι)

theorem Diffeology.IsPlot.dSmooth {X : Type u_1} [DiffeologicalSpace X] {n : ℕ} {p : EuclideanSpace ℝ (Fin n) → X} (hp : IsPlot p) : DSmooth p

theorem Diffeology.DSmooth.isPlot {X : Type u_1} [DiffeologicalSpace X] {n : ℕ} {p : EuclideanSpace ℝ (Fin n) → X} (hp : DSmooth p) : IsPlot p

theorem Diffeology.isPlot_iff_dSmooth {X : Type u_1} [DiffeologicalSpace X] {n : ℕ} {p : EuclideanSpace ℝ (Fin n) → X} : IsPlot p ↔ DSmooth p

theorem Diffeology.isPlot_id {n : ℕ} : IsPlot id

theorem Diffeology.isPlot_id' {n : ℕ} : IsPlot fun (x : EuclideanSpace ℝ (Fin n)) => x

theorem Diffeology.isPlot_iff_contDiff {X : Type u_1} [DiffeologicalSpace X] {n : ℕ} [NormedAddCommGroup X] [NormedSpace ℝ X] [IsContDiffCompatible X] {p : EuclideanSpace ℝ (Fin n) → X} : IsPlot p ↔ ContDiff ℝ (↑⊤) p

theorem ContDiff.isPlot {X : Type u_1} [DiffeologicalSpace X] {n : ℕ} [NormedAddCommGroup X] [NormedSpace ℝ X] [Diffeology.IsContDiffCompatible X] {p : EuclideanSpace ℝ (Fin n) → X} (hp : ContDiff ℝ (↑⊤) p) : Diffeology.IsPlot p

theorem Diffeology.IsPlot.contDiff {X : Type u_1} [DiffeologicalSpace X] {n : ℕ} [NormedAddCommGroup X] [NormedSpace ℝ X] [IsContDiffCompatible X] {p : EuclideanSpace ℝ (Fin n) → X} (hp : IsPlot p) : ContDiff ℝ (↑⊤) p

theorem ContDiff.dSmooth {X : Type u_1} [DiffeologicalSpace X] {Y : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [Diffeology.IsContDiffCompatible X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] [DiffeologicalSpace Y] [Diffeology.IsContDiffCompatible Y] {f : X → Y} (hf : ContDiff ℝ (↑⊤) f) : Diffeology.DSmooth f

theorem Diffeology.DSmooth.contDiff {X : Type u_1} [DiffeologicalSpace X] {Y : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [IsContDiffCompatible X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] [DiffeologicalSpace Y] [IsContDiffCompatible Y] [FiniteDimensional ℝ X] {f : X → Y} (hf : DSmooth f) : ContDiff ℝ (↑⊤) f

theorem Diffeology.dSmooth_iff_contDiff {X : Type u_1} [DiffeologicalSpace X] {Y : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [IsContDiffCompatible X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] [DiffeologicalSpace Y] [IsContDiffCompatible Y] [FiniteDimensional ℝ X] {f : X → Y} : DSmooth f ↔ ContDiff ℝ (↑⊤) f