OAI/Combinatorics/IndependentSets/Expansion/PreprocessingStageMaps.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.IndependentSetsGames.Foundations.PCP.PreprocessingStageMaps.BaseTable line 9
  2. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingStageMaps.regular line 11
  3. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingStageMaps.padding line 14
  4. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingStageMaps.familyAt line 18
  5. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingStageMaps.paddedOverlay line 23
  6. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingStageMaps.lazy line 28
  7. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingStageMaps.output_eq line 31