Theorems · Theorem · global analysis

DiffeologicalSpace.locality

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

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

Defined in

Mathlib.Geometry.Diffeology.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

DiffeologicalSpace