OAI/Combinatorics/Ryser/Incidence/FiniteSetEstimates.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RyserCoveringCounterexample.Incidence.FiniteSetEstimates.ruzsa_triangle_inequality_div_div_div line 28
2. theorem OAI.RyserCoveringCounterexample.Incidence.FiniteSetEstimates.ruzsa_triangle_inequality_div_mul_mul line 33
3. theorem OAI.RyserCoveringCounterexample.Incidence.FiniteSetEstimates.pluennecke_petridis_inequality_mul line 38
4. theorem OAI.RyserCoveringCounterexample.Incidence.FiniteSetEstimates.mul_aux line 48
5. lemma OAI.RyserCoveringCounterexample.Incidence.FiniteSetEstimates.card_mul_pow_le line 54
6. theorem OAI.RyserCoveringCounterexample.Incidence.FiniteSetEstimates.pluennecke_ruzsa_inequality_pow_div_pow_mul line 60
7. theorem OAI.RyserCoveringCounterexample.Incidence.FiniteSetEstimates.pluennecke_ruzsa_inequality_pow_div_pow_div line 65