OAI/Combinatorics/BalancedRyser/Probability/PermutationSubsetLaw.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Balanced.PermutationSubsetLaw.expect_comp_of_fiber_card_eq line 9
  2. theorem OAI.Balanced.PermutationSubsetLaw.exists_perm_fixing_map line 46
  3. def OAI.Balanced.PermutationSubsetLaw.postcompose line 68
  4. theorem OAI.Balanced.PermutationSubsetLaw.target_image_fiber_card_eq line 74
  5. theorem OAI.Balanced.PermutationSubsetLaw.expect_image_conditioned_target line 104
  6. theorem OAI.Balanced.PermutationSubsetLaw.image_fiber_card_eq line 138
  7. theorem OAI.Balanced.PermutationSubsetLaw.expect_image line 157
  8. theorem OAI.Balanced.PermutationSubsetLaw.expect_two_images_conditioned_target line 173
  9. theorem OAI.Balanced.PermutationSubsetLaw.expect_eq_expect_fiber_of_card_eq line 191
  10. theorem OAI.Balanced.PermutationSubsetLaw.target_fiber_card_eq line 216
  11. theorem OAI.Balanced.PermutationSubsetLaw.expect_position line 233
  12. theorem OAI.Balanced.PermutationSubsetLaw.target_probability line 244
  13. theorem OAI.Balanced.PermutationSubsetLaw.expect_by_target line 251