OAI/Geometry/SurfaceImmersion/Primitive/CircularPrefixMetrics.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

The actual ordered prefix metrics of a finite circular family.

  1. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.metric_eq_of_inner_eq line 26
  2. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.CircularPrimitiveFamily.totalTensor line 35
  3. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.CircularPrimitiveFamily.smoothFamily line 38
  4. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.CircularPrimitiveFamily.prefixIndices line 45
  5. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.CircularPrimitiveFamily.prefixIndices_zero line 48
  6. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.CircularPrimitiveFamily.prefixIndices_last line 52
  7. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.CircularPrimitiveFamily.prefixIndices_step line 56
  8. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.CircularPrimitiveFamily.not_mem_prefixIndices line 68
  9. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.CircularPrimitiveFamily.prefixMetric line 71
  10. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.CircularPrimitiveFamily.prefixMetric_inner line 75
  11. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.CircularPrimitiveFamily.prefixMetric_zero line 83
  12. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.CircularPrimitiveFamily.prefixMetric_step line 90
  13. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.CircularPrimitiveFamily.prefixMetric_last line 99
  14. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.CircularPrimitiveFamily.realize_total line 104