OAI/Geometry/PrescribedPotential/PathMetricCompactC1.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Path Metric Compact C1.

  1. structure OAI.Anticanonical.SourceSmooth.PathSolution line 18
  2. def OAI.Anticanonical.SourceSmooth.PathSolution.metric line 26
  3. lemma OAI.Anticanonical.SourceSmooth.path_metric_compact_C1 line 31