OAI/Combinatorics/BalancedRyser/Incidence/RepeatedIncidences.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Balanced.RepeatedIncidences.multiplicity line 12
2. def OAI.Balanced.RepeatedIncidences.reuse line 15
3. theorem OAI.Balanced.RepeatedIncidences.sum_multiplicity line 20
4. theorem OAI.Balanced.RepeatedIncidences.multiplicity_pos line 38
5. theorem OAI.Balanced.RepeatedIncidences.reuse_eq_sum line 45
6. theorem OAI.Balanced.RepeatedIncidences.mem_inter_rest_iff line 50
7. theorem OAI.Balanced.RepeatedIncidences.sum_inter_rest line 74
8. theorem OAI.Balanced.RepeatedIncidences.sum_inter_rest_le_twice_reuse line 102