Theorems · Definition · global analysis

Diffeology.IsPlot

{X : Type u_1} → [DiffeologicalSpace X] → {n : ℕ} → (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).

Defined in

Mathlib.Geometry.Diffeology.Basic

Cited by

29 results in Mathlib

Foundations

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

Assumes

DiffeologicalSpace