OAI/Combinatorics/KMedian/CookLevin/TableauDirectories.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MetricKMedian.PCP.Compiler.TableauDirectory.VC line 15
  2. abbrev OAI.MetricKMedian.PCP.Compiler.TableauDirectory.TC line 16
  3. def OAI.MetricKMedian.PCP.Compiler.TableauDirectory.varCode line 17
  4. def OAI.MetricKMedian.PCP.Compiler.TableauDirectory.clauseCode line 21
  5. def OAI.MetricKMedian.PCP.Compiler.TableauDirectory.boundaryCode line 27
  6. def OAI.MetricKMedian.PCP.Compiler.TableauDirectory.testCode line 31
  7. lemma OAI.MetricKMedian.PCP.Compiler.TableauDirectory.varCode_injective line 33
  8. lemma OAI.MetricKMedian.PCP.Compiler.TableauDirectory.clauseCode_injective line 46
  9. lemma OAI.MetricKMedian.PCP.Compiler.TableauDirectory.boundaryCode_injective line 52
  10. lemma OAI.MetricKMedian.PCP.Compiler.TableauDirectory.testCode_injective line 64
  11. def OAI.MetricKMedian.PCP.Compiler.TableauDirectory.varOrder line 73
  12. def OAI.MetricKMedian.PCP.Compiler.TableauDirectory.clauseOrder line 75
  13. def OAI.MetricKMedian.PCP.Compiler.TableauDirectory.boolOrder line 80
  14. def OAI.MetricKMedian.PCP.Compiler.TableauDirectory.boundaryOrder line 84
  15. def OAI.MetricKMedian.PCP.Compiler.TableauDirectory.testOrder line 86
  16. def OAI.MetricKMedian.PCP.Compiler.TableauDirectory.vars line 87
  17. def OAI.MetricKMedian.PCP.Compiler.TableauDirectory.clauses line 92
  18. def OAI.MetricKMedian.PCP.Compiler.TableauDirectory.boundaries line 100
  19. def OAI.MetricKMedian.PCP.Compiler.TableauDirectory.tests line 103
  20. lemma OAI.MetricKMedian.PCP.Compiler.TableauDirectory.map_finRange line 104
  21. lemma OAI.MetricKMedian.PCP.Compiler.TableauDirectory.flatMap_finRange line 109
  22. lemma OAI.MetricKMedian.PCP.Compiler.TableauDirectory.vars_correct line 112
  23. lemma OAI.MetricKMedian.PCP.Compiler.TableauDirectory.clauses_correct line 116
  24. lemma OAI.MetricKMedian.PCP.Compiler.TableauDirectory.boundaries_correct line 120
  25. lemma OAI.MetricKMedian.PCP.Compiler.TableauDirectory.tests_correct line 128