OAI/Combinatorics/IndependentSets/Reduction/Small.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LargeIndependentSets.Small line 9
  2. def OAI.LargeIndependentSets.Separated line 12
  3. def OAI.LargeIndependentSets.Aligned line 15
  4. structure OAI.LargeIndependentSets.LayerLaw line 20
  5. def OAI.LargeIndependentSets.LayerLaw.badMass line 26
  6. def OAI.LargeIndependentSets.DistributionalAlignment line 31
  7. def OAI.LargeIndependentSets.actualSlot line 41
  8. lemma OAI.LargeIndependentSets.actualSlot_some_mem line 46
  9. lemma OAI.LargeIndependentSets.actualSlot_unique line 54
  10. lemma OAI.LargeIndependentSets.actualSlot_exists line 69
  11. def OAI.LargeIndependentSets.actualPattern line 79
  12. lemma OAI.LargeIndependentSets.actualPattern_eq line 103
  13. lemma OAI.LargeIndependentSets.actualPattern_good_aligned line 111
  14. def OAI.LargeIndependentSets.ListSlot.pullbackFin line 138
  15. lemma OAI.LargeIndependentSets.ListSlot.map_pullbackFin line 143
  16. lemma OAI.LargeIndependentSets.good_full_restrict_goodOn line 155
  17. lemma OAI.LargeIndependentSets.good_embedding_restrict_goodOn line 178