OAI/Combinatorics/IndependentSets/Reduction/Simple.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LargeIndependentSets.Graph.ofSimple line 12
  2. theorem OAI.LargeIndependentSets.Graph.ofSimple_colorable line 19
  3. theorem OAI.LargeIndependentSets.Graph.ofSimple_independent line 27
  4. lemma OAI.LargeIndependentSets.Graph.exists_max_independent line 38
  5. theorem OAI.LargeIndependentSets.Graph.ofSimple_alpha line 47
  6. def OAI.LargeIndependentSets.Graph.clique line 60
  7. lemma OAI.LargeIndependentSets.Graph.clique_alpha_le line 67
  8. lemma OAI.LargeIndependentSets.Graph.clique_sound line 78
  9. def OAI.LargeIndependentSets.SamplerParameters.CliqueTest line 86
  10. def OAI.LargeIndependentSets.SamplerParameters.output line 91
  11. lemma OAI.LargeIndependentSets.SamplerParameters.output_complete line 96
  12. lemma OAI.LargeIndependentSets.SamplerParameters.output_size line 107
  13. theorem OAI.LargeIndependentSets.finite_graph_reduction line 120