OAI/RingTheory/BassTrace/MeasurableSlices.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.BassTrace.Sparse.measurable_intrinsicInterior_finite_hull line 17
  2. lemma OAI.BassTrace.Sparse.support_of_mem_original_hull line 39
  3. lemma OAI.BassTrace.Sparse.simplexCoordinates_full line 45
  4. lemma OAI.BassTrace.Sparse.marked_chart_pieces line 52
  5. lemma OAI.BassTrace.Sparse.IsLocallyConstant.measurable_uncurry line 137
  6. lemma OAI.BassTrace.Sparse.GraphGeometry.chartDistance_coordinates line 177
  7. lemma OAI.BassTrace.Sparse.GraphGeometry.coordinates_radius_inter line 194
  8. theorem OAI.BassTrace.Sparse.GraphGeometry.marked_ball_coarea line 210
  9. lemma OAI.BassTrace.Sparse.GraphGeometry.measurable_marked_ball_slices line 244
  10. lemma OAI.BassTrace.Sparse.GraphGeometry.measurable_marked_ball_slices_joint line 275
  11. theorem OAI.BassTrace.Sparse.GraphGeometry.integrated_marked_ball_coarea line 295