OAI/Combinatorics/BalancedRyser/Probability/SlotConditionedLaw.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Balanced.Slots.conditional_law_eq_uniformOn line 18
  2. theorem OAI.Balanced.Slots.conditional_law_eq_uniformOfFinset line 25
  3. theorem OAI.Balanced.Slots.conditional_law_real_finset line 37
  4. theorem OAI.Balanced.Slots.conditional_law_real_singleton line 44
  5. theorem OAI.Balanced.Slots.sum_conditional_law_real_singleton line 52
  6. theorem OAI.Balanced.Slots.conditional_law_real_singleton_pos_iff line 59
  7. theorem OAI.Balanced.Slots.law_real_pos_iff_nonempty line 69