OAI/Probability/SwitchChain/TripleCellTransport.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem315.TripleCellTransport.degreeCount_eq_degree line 14
  2. def OAI.Problem315.TripleCellTransport.splitGraph line 23
  3. theorem OAI.Problem315.TripleCellTransport.splitGraph_degree line 26
  4. abbrev OAI.Problem315.TripleCellTransport.Cell line 33
  5. abbrev OAI.Problem315.TripleCellTransport.Model line 40
  6. def OAI.Problem315.TripleCellTransport.referenceModel line 45
  7. def OAI.Problem315.TripleCellTransport.toModel line 48
  8. def OAI.Problem315.TripleCellTransport.modelState line 54
  9. theorem OAI.Problem315.TripleCellTransport.splitGraph_modelState line 61
  10. def OAI.Problem315.TripleCellTransport.fromModel line 66
  11. def OAI.Problem315.TripleCellTransport.cellEquiv line 71
  12. def OAI.Problem315.TripleCellTransport.referenceCell line 83
  13. def OAI.Problem315.TripleCellTransport.matrixEquiv line 86
  14. def OAI.Problem315.TripleCellTransport.pair line 94
  15. theorem OAI.Problem315.TripleCellTransport.split_mem_pair line 97
  16. theorem OAI.Problem315.TripleCellTransport.pair_eq_erase line 102
  17. theorem OAI.Problem315.TripleCellTransport.restrictions_map_iff line 121
  18. theorem OAI.Problem315.TripleCellTransport.sameFiber_iff_splitPairData line 144
  19. theorem OAI.Problem315.TripleCellTransport.cell_of_sameFiber line 153
  20. theorem OAI.Problem315.TripleCellTransport.sameFiber_iff_matrixRow line 166
  21. theorem OAI.Problem315.TripleCellTransport.cell_of_sameFiber_of_cell line 173
  22. theorem OAI.Problem315.TripleCellTransport.pair_card line 184
  23. theorem OAI.Problem315.TripleCellTransport.pair_mem_powersetCard line 187
  24. theorem OAI.Problem315.TripleCellTransport.pair_injective line 191
  25. def OAI.Problem315.TripleCellTransport.pairEquiv line 200
  26. theorem OAI.Problem315.TripleCellTransport.sum_pair line 212
  27. theorem OAI.Problem315.TripleCellTransport.sum_leftDegree_decompose line 218
  28. theorem OAI.Problem315.TripleCellTransport.cellData_iff_outsideGraph line 226
  29. theorem OAI.Problem315.TripleCellTransport.outsideGraph_eq_iff line 251
  30. def OAI.Problem315.TripleCellTransport.outsideCellEquiv line 262