OAI/Combinatorics/BalancedRyser/Selection/SelectionOccupancy.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Balanced.SelectionOccupancy.secondConstituents line 17
  2. def OAI.Balanced.SelectionOccupancy.initial line 20
  3. def OAI.Balanced.SelectionOccupancy.final line 24
  4. lemma OAI.Balanced.SelectionOccupancy.initial_subset_line line 27
  5. lemma OAI.Balanced.SelectionOccupancy.final_subset_initial line 33
  6. theorem OAI.Balanced.SelectionOccupancy.initial_card_lower_bound line 36
  7. lemma OAI.Balanced.SelectionOccupancy.mem_secondConstituents_iff line 49
  8. lemma OAI.Balanced.SelectionOccupancy.secondConstituent_mem line 54
  9. lemma OAI.Balanced.SelectionOccupancy.final_eq_initial_inter_retained line 58
  10. lemma OAI.Balanced.SelectionOccupancy.mem_core_iff line 71
  11. theorem OAI.Balanced.SelectionOccupancy.final_eq_core_inter line 87
  12. theorem OAI.Balanced.SelectionOccupancy.final_secondConstituent line 96
  13. theorem OAI.Balanced.SelectionOccupancy.occupancy_of_final line 106
  14. lemma OAI.Balanced.SelectionOccupancy.initialDeletedLines_eq line 117
  15. lemma OAI.Balanced.SelectionOccupancy.initiallyRetained_inter_line line 119
  16. lemma OAI.Balanced.SelectionOccupancy.constituent_multiplicity_le_sampled line 125
  17. theorem OAI.Balanced.SelectionOccupancy.candidate_good_initial line 135
  18. theorem OAI.Balanced.SelectionOccupancy.occupancy_of_candidate_good_final line 147