OAI/Combinatorics/KMedian/Programs/BundleGeometryProgram.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MetricKMedian.Preparation.RationalBundles.Program.Raw line 15
  2. def OAI.MetricKMedian.Preparation.RationalBundles.Program.view line 16
  3. def OAI.MetricKMedian.Preparation.RationalBundles.Program.neighborMask line 20
  4. theorem OAI.MetricKMedian.Preparation.RationalBundles.Program.neighborMask_poly line 21
  5. theorem OAI.MetricKMedian.Preparation.RationalBundles.Program.neighborMask_view line 22
  6. def OAI.MetricKMedian.Preparation.RationalBundles.Program.nextData line 27
  7. theorem OAI.MetricKMedian.Preparation.RationalBundles.Program.nextData_poly line 28
  8. theorem OAI.MetricKMedian.Preparation.RationalBundles.Program.nextData_view line 29
  9. def OAI.MetricKMedian.Preparation.RationalBundles.Program.bundleData line 39
  10. theorem OAI.MetricKMedian.Preparation.RationalBundles.Program.bundleData_poly line 45
  11. theorem OAI.MetricKMedian.Preparation.RationalBundles.Program.bundleData_view line 51
  12. def OAI.MetricKMedian.Preparation.RationalBundles.Program.bundlesData line 62
  13. theorem OAI.MetricKMedian.Preparation.RationalBundles.Program.bundlesData_poly line 63
  14. theorem OAI.MetricKMedian.Preparation.RationalBundles.Program.bundlesData_view line 64
  15. def OAI.MetricKMedian.Preparation.RationalBundles.Program.missingData line 72
  16. theorem OAI.MetricKMedian.Preparation.RationalBundles.Program.missingData_poly line 74
  17. theorem OAI.MetricKMedian.Preparation.RationalBundles.Program.missingData_view line 78
  18. def OAI.MetricKMedian.Preparation.RationalBundles.Program.massData line 87
  19. theorem OAI.MetricKMedian.Preparation.RationalBundles.Program.massData_poly line 89
  20. theorem OAI.MetricKMedian.Preparation.RationalBundles.Program.massData_view line 95