OAI/GroupTheory/PolycyclicRecognition/Geometry/FiniteCoordinateSmoothness.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Smoothness in a finite-dimensional space of functions

Point evaluations span the dual of a finite-dimensional function space. Consequently scalar pointwise smoothness detects smoothness into that space.

  1. def OAI.PolycyclicRecognition.coordinateEvaluation line 22
  2. theorem OAI.PolycyclicRecognition.span_coordinateEvaluation line 27
  3. theorem OAI.PolycyclicRecognition.contDiff_of_coordinateEvaluations line 45