OAI/Combinatorics/BalancedRyser/Local/InjectionExposure.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Balanced.InjectionExposure.completions line 10
  2. def OAI.Balanced.InjectionExposure.remaining line 13
  3. theorem OAI.Balanced.InjectionExposure.mem_completions line 16
  4. theorem OAI.Balanced.InjectionExposure.mem_remaining line 21
  5. theorem OAI.Balanced.InjectionExposure.completions_nonempty line 25
  6. theorem OAI.Balanced.InjectionExposure.value_mem_remaining line 29
  7. theorem OAI.Balanced.InjectionExposure.base_mem_remaining line 38
  8. theorem OAI.Balanced.InjectionExposure.card_remaining line 43
  9. theorem OAI.Balanced.InjectionExposure.swap_mem_completions line 48
  10. theorem OAI.Balanced.InjectionExposure.fibre_card_eq line 62
  11. theorem OAI.Balanced.InjectionExposure.card_completions_eq line 88
  12. theorem OAI.Balanced.InjectionExposure.next_value_probability line 105
  13. theorem OAI.Balanced.InjectionExposure.next_value_probability_card line 123
  14. theorem OAI.Balanced.InjectionExposure.event_card_eq line 129
  15. theorem OAI.Balanced.InjectionExposure.next_event_probability line 160
  16. theorem OAI.Balanced.InjectionExposure.next_event_probability_le line 185
  17. theorem OAI.Balanced.InjectionExposure.next_event_probability_le_budget line 193