OAI/Combinatorics/BalancedRyser/Candidates/CandidatePrescriptionTransport.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Balanced.CandidateRetentionTransport.mem_successfulChoices line 14
2. theorem OAI.Balanced.CandidateRetentionTransport.exists_successful_prescription line 22
3. theorem OAI.Balanced.CandidateRetentionTransport.prescription_choice_mem_successful line 42
4. theorem OAI.Balanced.CandidateRetentionTransport.successfulTest_at_target_eq_image line 49
5. theorem OAI.Balanced.CandidateRetentionTransport.successfulTest_at_target_card line 67
6. theorem OAI.Balanced.CandidateRetentionTransport.successfulTest_card_eq_sum_prescriptions line 74