OAI/Combinatorics/KMedian/Machines/AlphabetIndex.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.MetricKMedian.PCP.Compiler.AlphabetProgram.sampleCoding line 13
  2. instance OAI.MetricKMedian.PCP.Compiler.AlphabetProgram.sampleHardcoded line 14
  3. instance OAI.MetricKMedian.PCP.Compiler.AlphabetProgram.sampleInhabited line 15
  4. abbrev OAI.MetricKMedian.PCP.Compiler.AlphabetProgram.Tag line 16
  5. def OAI.MetricKMedian.PCP.Compiler.AlphabetProgram.B line 17
  6. def OAI.MetricKMedian.PCP.Compiler.AlphabetProgram.I line 18
  7. def OAI.MetricKMedian.PCP.Compiler.AlphabetProgram.S line 19
  8. def OAI.MetricKMedian.PCP.Compiler.AlphabetProgram.bitIndex line 20
  9. def OAI.MetricKMedian.PCP.Compiler.AlphabetProgram.intIndex line 21
  10. def OAI.MetricKMedian.PCP.Compiler.AlphabetProgram.sampleIndex line 22
  11. def OAI.MetricKMedian.PCP.Compiler.AlphabetProgram.nodeEquiv line 23
  12. lemma OAI.MetricKMedian.PCP.Compiler.AlphabetProgram.nodeEquiv_vertex line 30
  13. lemma OAI.MetricKMedian.PCP.Compiler.AlphabetProgram.nodeEquiv_interior line 32
  14. lemma OAI.MetricKMedian.PCP.Compiler.AlphabetProgram.nodeEquiv_test line 34
  15. abbrev OAI.MetricKMedian.PCP.Compiler.AlphabetProgram.Label line 36
  16. def OAI.MetricKMedian.PCP.Compiler.AlphabetProgram.positionInfo line 37
  17. def OAI.MetricKMedian.PCP.Compiler.AlphabetProgram.info line 41
  18. def OAI.MetricKMedian.PCP.Compiler.AlphabetProgram.allowed line 43
  19. lemma OAI.MetricKMedian.PCP.Compiler.AlphabetProgram.poly_info line 46
  20. lemma OAI.MetricKMedian.PCP.Compiler.AlphabetProgram.poly_allowed line 47
  21. lemma OAI.MetricKMedian.PCP.Compiler.AlphabetProgram.poly_sampleIndex line 48
  22. def OAI.MetricKMedian.PCP.Compiler.AlphabetProgram.endpoint line 49
  23. def OAI.MetricKMedian.PCP.Compiler.AlphabetProgram.row line 51
  24. lemma OAI.MetricKMedian.PCP.Compiler.AlphabetProgram.poly_endpoint line 55
  25. lemma OAI.MetricKMedian.PCP.Compiler.AlphabetProgram.poly_row line 63