OAI/Combinatorics/BalancedRyser/Probability/SlotEdges2.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Balanced.Slots.edgeEvent_mk line 17
  2. theorem OAI.Balanced.Slots.edgeSupport_mk line 22
  3. theorem OAI.Balanced.Slots.edgeSlotsDistinct_mk line 28
  4. theorem OAI.Balanced.Slots.edgeMass_mk line 31
  5. theorem OAI.Balanced.Slots.edgeEvent_dependsOn line 35
  6. theorem OAI.Balanced.Slots.law_real_edgeEvent line 45
  7. theorem OAI.Balanced.Slots.mem_supportNeighbors line 54
  8. theorem OAI.Balanced.Slots.mem_touching line 60
  9. theorem OAI.Balanced.Slots.support_neighbor_independence line 65
  10. theorem OAI.Balanced.Slots.cylinder_avoidance_independence line 83
  11. theorem OAI.Balanced.Slots.local_lemma_of_supports line 102
  12. theorem OAI.Balanced.Slots.local_lemma_cylinder_of_supports line 118
  13. theorem OAI.Balanced.Slots.conditional_law_real line 147
  14. theorem OAI.Balanced.Slots.conditional_law_zero_of_disjoint line 156