OAI/Combinatorics/IndependentSets/Reduction/FrameNonempty.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.LargeIndependentSets.Normalization.frame_nonempty line 14
  2. lemma OAI.LargeIndependentSets.Normalization.clauseBits_positive line 17
  3. lemma OAI.LargeIndependentSets.Normalization.clauses_le_input line 22
  4. lemma OAI.LargeIndependentSets.Normalization.names_bound line 35
  5. lemma OAI.LargeIndependentSets.Normalization.normalize_variables line 49
  6. lemma OAI.LargeIndependentSets.Normalization.normalize_clauses line 55
  7. lemma OAI.LargeIndependentSets.Normalization.normalize_bits line 69
  8. def OAI.LargeIndependentSets.LCInput.fallback line 90
  9. lemma OAI.LargeIndependentSets.LCInput.fallback_satisfies line 93
  10. lemma OAI.LargeIndependentSets.LCInput.honest_consistent line 97
  11. lemma OAI.LargeIndependentSets.LCInput.fallback_consistent line 103
  12. def OAI.LargeIndependentSets.LCInput.repair line 106
  13. lemma OAI.LargeIndependentSets.LCInput.repair_spec line 109
  14. lemma OAI.LargeIndependentSets.LCInput.repair_honest line 116
  15. def OAI.LargeIndependentSets.LCInput.repaired line 120
  16. def OAI.LargeIndependentSets.LCInput.labelCover line 123
  17. lemma OAI.LargeIndependentSets.LCInput.complete line 131
  18. lemma OAI.LargeIndependentSets.LCInput.repaired_accepts_iff line 145
  19. lemma OAI.LargeIndependentSets.LCInput.probability_expectation line 158
  20. lemma OAI.LargeIndependentSets.LCInput.success_eq line 163
  21. lemma OAI.LargeIndependentSets.LCInput.sound_of_value line 175
  22. theorem OAI.LargeIndependentSets.LCInput.uniform_repetition line 189