OAI/RingTheory/BassTrace/SimplexCoordinates.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.BassTrace.Sparse.barycentricParam_potential line 15
  2. lemma OAI.BassTrace.Sparse.treeParam_potential line 22
  3. lemma OAI.BassTrace.Sparse.treeArea_coarea line 31
  4. lemma OAI.BassTrace.Sparse.measurable_treeArea_slices line 66
  5. lemma OAI.BassTrace.Sparse.simplexArea_coarea line 98
  6. lemma OAI.BassTrace.Sparse.measurable_simplexArea_slices line 124
  7. lemma OAI.BassTrace.Sparse.simplexEmbed_nonneg line 150
  8. lemma OAI.BassTrace.Sparse.simplexEmbed_total line 162
  9. def OAI.BassTrace.Sparse.simplexPoint line 172
  10. def OAI.BassTrace.Sparse.chartDistance line 180
  11. lemma OAI.BassTrace.Sparse.chartDistance_apply line 184
  12. lemma OAI.BassTrace.Sparse.ballBranch_coordinates line 190
  13. def OAI.BassTrace.Sparse.distancePotential line 215
  14. lemma OAI.BassTrace.Sparse.distancePotential_edge line 221
  15. lemma OAI.BassTrace.Sparse.chartDistance_max line 233
  16. theorem OAI.BassTrace.Sparse.graphBall_coarea line 258
  17. lemma OAI.BassTrace.Sparse.measurable_graphBall_slices line 281