OAI/Probability/SwitchChain/FourVertexSwitch.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem315.FourDistinct line 9
  2. def OAI.Problem315.twoEdgeGraph line 12
  3. theorem OAI.Problem315.twoEdgeGraph_matching line 29
  4. def OAI.Problem315.fourVertexProposal line 64
  5. theorem OAI.Problem315.removedMatching_fourVertexProposal line 83
  6. theorem OAI.Problem315.addedMatching_fourVertexProposal line 91
  7. theorem OAI.Problem315.validSwitch_fourVertexProposal_iff line 99
  8. theorem OAI.Problem315.proposalResult_fourVertex_adj line 123
  9. theorem OAI.Problem315.switchStep_of_fourVertex_result line 138
  10. theorem OAI.Problem315.proposalResult_fourVertex_adj_first line 147
  11. theorem OAI.Problem315.proposalResult_fourVertex_adj_outside line 156
  12. def OAI.Problem315.fourVertexState line 165
  13. theorem OAI.Problem315.switchStep_fourVertexState line 170
  14. theorem OAI.Problem315.fourVertexState_agrees_outside line 177