OAI/Computability/PerfectCompleteness/Foundations/OutputAnnihilator.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PerfectCompleteness.OutputAnnihilator.bad line 18
  2. theorem OAI.PerfectCompleteness.OutputAnnihilator.mem_bad line 22
  3. theorem OAI.PerfectCompleteness.OutputAnnihilator.not_mem_bad_iff line 27
  4. theorem OAI.PerfectCompleteness.OutputAnnihilator.card_bad line 31
  5. theorem OAI.PerfectCompleteness.OutputAnnihilator.card_dual line 41
  6. theorem OAI.PerfectCompleteness.OutputAnnihilator.card_dual_eq_bad_mul line 45
  7. theorem OAI.PerfectCompleteness.OutputAnnihilator.bad_fraction line 49
  8. theorem OAI.PerfectCompleteness.OutputAnnihilator.bad_fraction_le_of_finrank_le line 58
  9. theorem OAI.PerfectCompleteness.OutputAnnihilator.bad_fraction_le_of_dimension_bound line 65
  10. theorem OAI.PerfectCompleteness.OutputAnnihilator.bad_fraction_le_of_codim_le line 71
  11. theorem OAI.PerfectCompleteness.OutputAnnihilator.bad_fraction_lt_of_codim_le line 85
  12. def OAI.PerfectCompleteness.OutputAnnihilator.badMasks line 94
  13. theorem OAI.PerfectCompleteness.OutputAnnihilator.mem_badMasks line 99
  14. theorem OAI.PerfectCompleteness.OutputAnnihilator.not_mem_badMasks_iff line 105
  15. theorem OAI.PerfectCompleteness.OutputAnnihilator.card_badMasks line 111
  16. theorem OAI.PerfectCompleteness.OutputAnnihilator.badMasks_fraction line 125
  17. theorem OAI.PerfectCompleteness.OutputAnnihilator.badMasks_fraction_lt_of_codim_le line 130