OAI/Combinatorics/IndependentSets/Reduction/Mixed.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LargeIndependentSets.ExplicitEnum.mixed line 9
  2. def OAI.LargeIndependentSets.ExplicitEnum.question line 13
  3. def OAI.LargeIndependentSets.ExplicitEnum.grid line 17
  4. def OAI.LargeIndependentSets.ExplicitEnum.equiv line 24
  5. lemma OAI.LargeIndependentSets.ExplicitEnum.length_eq_card line 27
  6. def OAI.LargeIndependentSets.rotationCode line 37
  7. def OAI.LargeIndependentSets.sampleLocationCode line 39
  8. lemma OAI.LargeIndependentSets.sampleLocationCode_eq line 50
  9. instance OAI.LargeIndependentSets.layeredImposedDecidable line 55
  10. def OAI.LargeIndependentSets.SamplerParameters.locationCode line 65
  11. lemma OAI.LargeIndependentSets.SamplerParameters.locationCode_eq line 69
  12. def OAI.LargeIndependentSets.SamplerParameters.chainEnumeration line 73
  13. def OAI.LargeIndependentSets.SamplerParameters.graphAdjDecidable line 78
  14. def OAI.LargeIndependentSets.SamplerParameters.cliqueDecidable line 91
  15. def OAI.LargeIndependentSets.SamplerParameters.enumeratedGraph line 107
  16. def OAI.LargeIndependentSets.SamplerParameters.enumeratedOutput line 122
  17. structure OAI.LargeIndependentSets.Graph.Renaming line 138
  18. def OAI.LargeIndependentSets.Graph.Renaming.symm line 145
  19. lemma OAI.LargeIndependentSets.Graph.Renaming.vertices_eq line 149
  20. lemma OAI.LargeIndependentSets.Graph.Renaming.independent line 152
  21. lemma OAI.LargeIndependentSets.Graph.Renaming.independent_card_le line 160
  22. lemma OAI.LargeIndependentSets.Graph.Renaming.alpha_le line 165
  23. lemma OAI.LargeIndependentSets.Graph.Renaming.alpha_eq line 170
  24. lemma OAI.LargeIndependentSets.Graph.Renaming.colorable line 173
  25. lemma OAI.LargeIndependentSets.Graph.Renaming.strict_density line 180