OAI/Combinatorics/BalancedRyser/Probability/CoreRepresentativeEquivalence.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Balanced.Configuration.eq_of_common_coreRepresentative line 14
  2. theorem OAI.Balanced.Configuration.coreRepresentative_disjoint line 39
  3. theorem OAI.Balanced.Configuration.filtered_representatives_card_eq line 46
  4. theorem OAI.Balanced.Configuration.representatives_card_eq_nonempty line 70
  5. theorem OAI.Balanced.Configuration.pencil_representatives_card_eq_labels line 83
  6. theorem OAI.Balanced.Configuration.core_block_mem_iff_representative line 98
  7. theorem OAI.Balanced.Configuration.core_cover_iff_representative_cover line 116
  8. theorem OAI.Balanced.Configuration.existsUnique_label_of_not_deleted line 133
  9. theorem OAI.Balanced.Configuration.all_coreRepresentatives_eq_nondeleted line 153