Theorems · Theorem · global analysis

DiffeologicalSpace.plot_reparam

∀ {X : Type u_1} [self : DiffeologicalSpace X] {n m : ℕ} {p : EuclideanSpace ℝ (Fin m) → X}
  {f : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin m)},
  p ∈ DiffeologicalSpace.plots m → ContDiff ℝ (↑⊤) f → p ∘ f ∈ DiffeologicalSpace.plots n

Smooth reparametrisations of plots need to be plots.

Defined in

Mathlib.Geometry.Diffeology.Basic

Cited by

1 results in Mathlib

Foundations

Depth 226 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DiffeologicalSpace