OAI/Combinatorics/Ryser/Construction/AmbientDeletionTrials.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RyserCoveringCounterexample.Construction.ambientTrialOutcome line 19
  2. def OAI.RyserCoveringCounterexample.Construction.ambientTrialLaw line 26
  3. def OAI.RyserCoveringCounterexample.Construction.ambientPointRate line 32
  4. theorem OAI.RyserCoveringCounterexample.Construction.ambientTrialLaw_point_probability line 35
  5. theorem OAI.RyserCoveringCounterexample.Construction.ambientPointRate_le line 43
  6. theorem OAI.RyserCoveringCounterexample.Construction.ambientTrialLaw_line_probability_le line 51
  7. abbrev OAI.RyserCoveringCounterexample.Construction.AmbientPosition line 72
  8. def OAI.RyserCoveringCounterexample.Construction.ambientTrialCount line 74
  9. def OAI.RyserCoveringCounterexample.Construction.ambientPosition line 76
  10. def OAI.RyserCoveringCounterexample.Construction.ambientTrials line 79
  11. theorem OAI.RyserCoveringCounterexample.Construction.ambientTrialCount_mul_sub_one_le line 86
  12. theorem OAI.RyserCoveringCounterexample.Construction.ambientTrialCount_le line 97
  13. theorem OAI.RyserCoveringCounterexample.Construction.ambientTrials_line_probability_sum_le line 107