OAI/Combinatorics/BalancedRyser/Probability/CoreRepresentatives.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Balanced.Configuration.coreRepresentative line 17
  2. lemma OAI.Balanced.Configuration.mem_constituentLines line 23
  3. lemma OAI.Balanced.Configuration.constituent_not_split line 28
  4. lemma OAI.Balanced.Configuration.false_constituent_not_deleted line 38
  5. lemma OAI.Balanced.Configuration.core_avoids_deleted line 49
  6. lemma OAI.Balanced.Configuration.split_mem_deleted line 54
  7. lemma OAI.Balanced.Configuration.tuplePoint_not_core line 59
  8. theorem OAI.Balanced.Configuration.core_block_has_representative line 65
  9. lemma OAI.Balanced.Configuration.core_subset_points_for_representatives line 94
  10. lemma OAI.Balanced.Configuration.coreRepresentative_card_le_one line 104
  11. lemma OAI.Balanced.Configuration.coreRepresentative_not_deleted line 108
  12. theorem OAI.Balanced.Configuration.representatives_card_le line 126
  13. theorem OAI.Balanced.Configuration.core_cover_reduction line 131
  14. def OAI.Balanced.Configuration.RepresentedThrough line 147
  15. lemma OAI.Balanced.Configuration.pencil_representatives_card_le_labels line 151
  16. lemma OAI.Balanced.Configuration.outside_pencil_representatives_card_le_labels line 165
  17. theorem OAI.Balanced.Configuration.core_cover_outside_pencil_budget line 182