OAI/Combinatorics/BalancedRyser/Local/InjectionExposureLaw.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Balanced.InjectionExposureLaw.history line 14
  2. def OAI.Balanced.InjectionExposureLaw.available line 17
  3. theorem OAI.Balanced.InjectionExposureLaw.mem_history line 20
  4. theorem OAI.Balanced.InjectionExposureLaw.self_mem_history line 23
  5. theorem OAI.Balanced.InjectionExposureLaw.mem_available line 27
  6. def OAI.Balanced.InjectionExposureLaw.postcompose line 30
  7. theorem OAI.Balanced.InjectionExposureLaw.postcompose_apply line 37
  8. theorem OAI.Balanced.InjectionExposureLaw.next_fiber_card_eq line 40
  9. theorem OAI.Balanced.InjectionExposureLaw.next_mem_available line 67
  10. theorem OAI.Balanced.InjectionExposureLaw.expect_next_given_history line 75
  11. theorem OAI.Balanced.InjectionExposureLaw.card_available line 89
  12. theorem OAI.Balanced.InjectionExposureLaw.next_probability_given_history line 93
  13. theorem OAI.Balanced.InjectionExposureLaw.range_fiber_card_eq line 104
  14. theorem OAI.Balanced.InjectionExposureLaw.expect_range line 123
  15. def OAI.Balanced.InjectionExposureLaw.selfEmbeddingEquivPerm line 139
  16. def OAI.Balanced.InjectionExposureLaw.permutationHistory line 145
  17. theorem OAI.Balanced.InjectionExposureLaw.expect_permutation_next_given_history line 149