OAI/Combinatorics/IndependentSets/Reduction/DeletedProjection.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LargeIndependentSets.deletedProjection line 17
  2. lemma OAI.LargeIndependentSets.deleted_phase_reindex line 23
  3. def OAI.LargeIndependentSets.ruleUnion line 39
  4. lemma OAI.LargeIndependentSets.mem_ruleUnion line 45
  5. lemma OAI.LargeIndependentSets.aligned_excludes_deleted line 54
  6. def OAI.LargeIndependentSets.deletedRule line 78
  7. lemma OAI.LargeIndependentSets.actual_deleted_junta line 87
  8. def OAI.LargeIndependentSets.fiberSquare line 126
  9. theorem OAI.LargeIndependentSets.actual_aligned_fiber line 134