OAI/Combinatorics/BalancedRyser/Probability/SlotProbability2.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.Balanced.Slots.law_isProbabilityMeasure line 18
  2. theorem OAI.Balanced.Slots.independent_coordinates line 24
  3. theorem OAI.Balanced.Slots.law_cylinder line 28
  4. theorem OAI.Balanced.Slots.law_real_cylinder line 38
  5. theorem OAI.Balanced.Slots.law_real_cylinder_pos line 42
  6. theorem OAI.Balanced.Slots.independent_restrictions line 51
  7. theorem OAI.Balanced.Slots.dependsOn_representation line 58
  8. theorem OAI.Balanced.Slots.independent_events_of_disjoint line 72
  9. theorem OAI.Balanced.Slots.law_real_inter_of_disjoint line 86
  10. theorem OAI.Balanced.Slots.cylinder_dependsOn line 95
  11. theorem OAI.Balanced.Slots.DependsOn.compl line 107
  12. theorem OAI.Balanced.Slots.dependsOn_biInter line 115
  13. theorem OAI.Balanced.Slots.pairEvent_dependsOn line 129
  14. theorem OAI.Balanced.Slots.law_eq_uniformOn line 137
  15. theorem OAI.Balanced.Slots.law_coordinate line 148
  16. theorem OAI.Balanced.Slots.law_pairEvent line 156
  17. theorem OAI.Balanced.Slots.law_real_pairEvent line 166
  18. theorem OAI.Balanced.Slots.law_real_inter_avoidance line 171
  19. theorem OAI.Balanced.Slots.law_real_finset line 189