OAI/Geometry/SplitTangent/EmbeddedPlaqueChart.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Embedded Plaque Chart.

  1. structure OAI.EmbeddedPlaqueChart.Data line 14
  2. def OAI.EmbeddedPlaqueChart.Data.inverse line 31
  3. lemma OAI.EmbeddedPlaqueChart.Data.inverse_val line 36
  4. lemma OAI.EmbeddedPlaqueChart.Data.inverse_continuousAt line 39
  5. def OAI.EmbeddedPlaqueChart.Data.chart line 52
  6. lemma OAI.EmbeddedPlaqueChart.Data.chart_mem line 87
  7. lemma OAI.EmbeddedPlaqueChart.Data.chart_source line 88
  8. lemma OAI.EmbeddedPlaqueChart.Data.chart_target line 90
  9. lemma OAI.EmbeddedPlaqueChart.Data.chart_apply line 91
  10. lemma OAI.EmbeddedPlaqueChart.Data.chart_inverse_val line 92