OAI/Combinatorics/BalancedRyser/Candidates/CandidateOccupancyBridge.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Balanced.candidateTrackedSets line 14
2. theorem OAI.Balanced.candidateTrackedSets_eq line 17
3. theorem OAI.Balanced.candidateSelection_trackedSets line 20
4. theorem OAI.Balanced.candidateSelection_output_line line 26
5. theorem OAI.Balanced.candidateSelection_finalTracked line 37
6. theorem OAI.Balanced.candidateSelection_occupancy_of_no_failure line 49
7. theorem OAI.Balanced.candidateSelection_occupancy_failure_mass_le line 65