OAI/Combinatorics/Ryser/Construction/AmbientDeletionNumerics.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.RyserCoveringCounterexample.Construction.ambientDeletionDelta line 15
2. theorem OAI.RyserCoveringCounterexample.Construction.ambientDeletionDelta_pos line 18
3. theorem OAI.RyserCoveringCounterexample.Construction.ambientDeletionDelta_lt_one line 21
4. theorem OAI.RyserCoveringCounterexample.Construction.neg_two_mul_le_log_one_sub line 32
5. theorem OAI.RyserCoveringCounterexample.Construction.exp_neg_two_mul_le_one_sub_pow line 47
6. theorem OAI.RyserCoveringCounterexample.Construction.ambientDeletionDelta_le_pow line 57
7. theorem OAI.RyserCoveringCounterexample.Construction.ambientDeletionDelta_le_finset_prod line 84
8. theorem OAI.RyserCoveringCounterexample.Construction.ambientDeletionDelta_le_prod line 105