OAI/Combinatorics/IndependentSets/Reduction/EnumerationSimple.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LargeIndependentSets.Graph.enumeration_to_simple line 12
  2. def OAI.LargeIndependentSets.SamplerParameters.decisionOutput_renaming line 27
  3. lemma OAI.LargeIndependentSets.SamplerParameters.enumeratedGraph_eq line 51
  4. def OAI.LargeIndependentSets.SamplerParameters.enumeratedOutput_renaming line 54
  5. lemma OAI.LargeIndependentSets.SamplerParameters.enumeratedOutput_complete line 60
  6. lemma OAI.LargeIndependentSets.SamplerParameters.enumeratedOutput_size_le line 65
  7. lemma OAI.LargeIndependentSets.SamplerParameters.enumeratedOutput_size_eq line 72
  8. theorem OAI.LargeIndependentSets.executable_finite_graph_reduction line 78
  9. def OAI.LargeIndependentSets.SamplerParameters.vertexEnumeration line 105
  10. lemma OAI.LargeIndependentSets.SamplerParameters.vertexEnumeration_nonempty line 116
  11. lemma OAI.LargeIndependentSets.SamplerParameters.vertexEnumeration_length line 124
  12. def OAI.LargeIndependentSets.SamplerParameters.namedOutput line 145
  13. def OAI.LargeIndependentSets.SamplerParameters.namedOutput_renaming line 159