OAI/Combinatorics/IndependentSets/PCP/TargetLC.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LargeIndependentSets.LabelCoverData.reindex line 12
  2. lemma OAI.LargeIndependentSets.LabelCoverData.reindex_complete line 18
  3. lemma OAI.LargeIndependentSets.LabelCoverData.reindex_sound line 25
  4. abbrev OAI.LargeIndependentSets.TargetLC.Input line 55
  5. lemma OAI.LargeIndependentSets.TargetLC.clauses_pos line 57
  6. lemma OAI.LargeIndependentSets.TargetLC.vars_pos line 58
  7. def OAI.LargeIndependentSets.TargetLC.eventEquiv line 62
  8. def OAI.LargeIndependentSets.TargetLC.table line 65
  9. lemma OAI.LargeIndependentSets.TargetLC.table_lc line 76
  10. lemma OAI.LargeIndependentSets.TargetLC.complete line 79
  11. lemma OAI.LargeIndependentSets.TargetLC.sound line 83
  12. lemma OAI.LargeIndependentSets.TargetLC.project_apply line 87