OAI/Combinatorics/BalancedRyser/Candidates/CandidateRetention.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Balanced.CandidateRetention.card_sq_le_image_card_mul_fiber_sq line 13
2. theorem OAI.Balanced.CandidateRetention.fiber_sq_sum_mono line 24
3. theorem OAI.Balanced.CandidateRetention.valid_card_sq_le_retained_mul_all_sq line 37
4. theorem OAI.Balanced.CandidateRetention.retained_card_lower_bound line 49