Theorems · Definition · global analysis

NormedSpace.toDiffeology

(X : Type u_1) →
  [inst : NormedAddCommGroup X] → [inst_1 : NormedSpace ℝ X] → [FiniteDimensional ℝ X] → DiffeologicalSpace X

Diffeology on a finite-dimensional normed space. We make this a definition instead of an instance because we also want to have product diffeologies as an instance, and having both would cause instance diamonds on spaces like Fin n → ℝ.

Defined in

Mathlib.Geometry.Diffeology.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceFiniteDimensional