OAI/Combinatorics/KMedian/Process/TaperReindex.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MetricKMedian.Taper.image_univ_reindex line 13
  2. theorem OAI.MetricKMedian.Taper.upper_reindex line 20
  3. theorem OAI.MetricKMedian.Taper.breaks_reindex line 22
  4. theorem OAI.MetricKMedian.Taper.a_reindex line 26
  5. theorem OAI.MetricKMedian.Taper.b_reindex line 28
  6. theorem OAI.MetricKMedian.Taper.candidates_reindex line 30
  7. theorem OAI.MetricKMedian.Taper.mass_reindex line 33
  8. theorem OAI.MetricKMedian.Taper.roots_reindex line 36
  9. theorem OAI.MetricKMedian.Taper.radius_reindex line 39
  10. theorem OAI.MetricKMedian.Taper.colocated_reindex line 42
  11. theorem OAI.MetricKMedian.Taper.zeros_reindex line 48
  12. theorem OAI.MetricKMedian.Taper.extend_reindex line 53
  13. theorem OAI.MetricKMedian.Taper.zeroMarginal_reindex line 64
  14. theorem OAI.MetricKMedian.Taper.source_reindex line 72