Theorems · Theorem · global analysis

Diffeology.isPlot_reparam

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

Defined in

Mathlib.Geometry.Diffeology.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

DiffeologicalSpace