OAI/Computability/PerfectCompleteness/Construction/LocalCompletionFamily.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.LocalCompletionFamily.Input line 14
  2. abbrev OAI.PerfectCompleteness.LocalCompletionFamily.Result line 16
  3. abbrev OAI.PerfectCompleteness.LocalCompletionFamily.Legal line 18
  4. def OAI.PerfectCompleteness.LocalCompletionFamily.legalEmbedding line 20
  5. def OAI.PerfectCompleteness.LocalCompletionFamily.legalProjection line 23
  6. def OAI.PerfectCompleteness.LocalCompletionFamily.Admissible line 25
  7. def OAI.PerfectCompleteness.LocalCompletionFamily.activeCount line 28
  8. theorem OAI.PerfectCompleteness.LocalCompletionFamily.activeCount_positive line 30
  9. theorem OAI.PerfectCompleteness.LocalCompletionFamily.activeCount_le line 33
  10. def OAI.PerfectCompleteness.LocalCompletionFamily.table line 36
  11. structure OAI.PerfectCompleteness.LocalCompletionFamily.Correct line 40
  12. def OAI.PerfectCompleteness.LocalCompletionFamily.packSampler line 47
  13. theorem OAI.PerfectCompleteness.LocalCompletionFamily.activeCount_packSampler line 52
  14. def OAI.PerfectCompleteness.LocalCompletionFamily.packedSeedEquiv line 58
  15. theorem OAI.PerfectCompleteness.LocalCompletionFamily.table_packSampler line 66
  16. theorem OAI.PerfectCompleteness.LocalCompletionFamily.uniformProbability_equiv line 76
  17. theorem OAI.PerfectCompleteness.LocalCompletionFamily.uniformProbability_packSampler line 84
  18. theorem OAI.PerfectCompleteness.LocalCompletionFamily.correct_packSampler line 105
  19. theorem OAI.PerfectCompleteness.LocalCompletionFamily.exists_correct line 131
  20. def OAI.PerfectCompleteness.LocalCompletionFamily.fallback line 157
  21. def OAI.PerfectCompleteness.LocalCompletionFamily.lookup line 160
  22. theorem OAI.PerfectCompleteness.LocalCompletionFamily.lookup_correct line 163