OAI/Combinatorics/KMedian/CookLevin/InitialAlphabet.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MetricKMedian.PCP.BinaryCSP.rejection_zero_iff line 16
  2. lemma OAI.MetricKMedian.PCP.AlphabetReduction.binary_iff line 24
  3. def OAI.MetricKMedian.PCP.InitialAlphabet.oneHot line 41
  4. lemma OAI.MetricKMedian.PCP.InitialAlphabet.oneHot_injective line 43
  5. def OAI.MetricKMedian.PCP.InitialAlphabet.decode line 49
  6. lemma OAI.MetricKMedian.PCP.InitialAlphabet.decode_oneHot line 51
  7. def OAI.MetricKMedian.PCP.InitialAlphabet.bits line 54
  8. lemma OAI.MetricKMedian.PCP.InitialAlphabet.bits_iff line 56
  9. def OAI.MetricKMedian.PCP.InitialAlphabet.reduced line 62
  10. lemma OAI.MetricKMedian.PCP.InitialAlphabet.reduced_iff line 64
  11. instance OAI.MetricKMedian.PCP.InitialAlphabet.edgeNonempty line 67
  12. def OAI.MetricKMedian.PCP.InitialAlphabet.box line 69
  13. lemma OAI.MetricKMedian.PCP.InitialAlphabet.box_iff line 70