OAI/Combinatorics/KMedian/Process/PhysicalHistoriesProgram.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MetricKMedian.RationalPhysicalKernel.HistoryProgram.Hist line 18
  2. def OAI.MetricKMedian.RationalPhysicalKernel.HistoryProgram.law line 19
  3. abbrev OAI.MetricKMedian.RationalPhysicalKernel.HistoryProgram.view line 20
  4. def OAI.MetricKMedian.RationalPhysicalKernel.HistoryProgram.result line 21
  5. def OAI.MetricKMedian.RationalPhysicalKernel.HistoryProgram.nextCtx line 23
  6. def OAI.MetricKMedian.RationalPhysicalKernel.HistoryProgram.nextRaw line 26
  7. theorem OAI.MetricKMedian.RationalPhysicalKernel.HistoryProgram.nextRaw_poly line 28
  8. theorem OAI.MetricKMedian.RationalPhysicalKernel.HistoryProgram.nextCtx_raw line 29
  9. def OAI.MetricKMedian.RationalPhysicalKernel.HistoryProgram.attach line 32
  10. theorem OAI.MetricKMedian.RationalPhysicalKernel.HistoryProgram.attach_poly line 34
  11. def OAI.MetricKMedian.RationalPhysicalKernel.HistoryProgram.inputs line 40
  12. theorem OAI.MetricKMedian.RationalPhysicalKernel.HistoryProgram.attach_result line 42
  13. theorem OAI.MetricKMedian.RationalPhysicalKernel.HistoryProgram.conditional line 48
  14. def OAI.MetricKMedian.RationalPhysicalKernel.HistoryProgram.program line 58