Theorems · Theorem · global analysis

Diffeology.IsPlot.dSmooth_comp

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

Defined in: Mathlib.Geometry.Diffeology.Basic
Cited by: 0 results in Mathlib
Foundations: Depth 121 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: DiffeologicalSpace DiffeologicalSpace

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites5

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Realstatement and proof · cited by 25,697
EuclideanSpacestatement and proof · cited by 307
DiffeologicalSpacestatement and proof · cited by 60
Diffeology.IsPlotstatement and proof · cited by 29
Diffeology.DSmoothstatement and proof · cited by 16

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.