OAI/Combinatorics/IndependentSets/Reduction/ThresholdDecidable.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LargeIndependentSets.ShortestPaths.thresholdDecidable line 10
  2. structure OAI.LargeIndependentSets.ExplicitEnum line 27
  3. def OAI.LargeIndependentSets.ExplicitEnum.ofCover line 34
  4. def OAI.LargeIndependentSets.ExplicitEnum.fin line 37
  5. def OAI.LargeIndependentSets.ExplicitEnum.sum line 40
  6. def OAI.LargeIndependentSets.ExplicitEnum.prod line 48
  7. def OAI.LargeIndependentSets.ExplicitEnum.sigma line 52
  8. def OAI.LargeIndependentSets.ExplicitEnum.pi line 58
  9. def OAI.LargeIndependentSets.ExplicitEnum.subtype line 67
  10. def OAI.LargeIndependentSets.ExplicitEnum.zmod line 74
  11. def OAI.LargeIndependentSets.enumerationEquiv line 82
  12. def OAI.LargeIndependentSets.Graph.ofEnumeration line 93
  13. lemma OAI.LargeIndependentSets.Graph.ofEnumeration_colorable line 101
  14. lemma OAI.LargeIndependentSets.Graph.ofEnumeration_independent line 110
  15. theorem OAI.LargeIndependentSets.Graph.ofEnumeration_alpha line 127