OAI/Probability/SpanningForest/FiniteUSTRelabel.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem336.relabelPair line 10
  2. def OAI.Problem336.relabelEdgeSet line 13
  3. def OAI.Problem336.relabelFiniteSubgraph line 16
  4. theorem OAI.Problem336.relabelPair_rawPair line 20
  5. theorem OAI.Problem336.relabelPair_edge line 29
  6. theorem OAI.Problem336.relabelPair_symm line 33
  7. theorem OAI.Problem336.relabelPair_injOn line 39
  8. theorem OAI.Problem336.relabelEdgeSet_card line 45
  9. theorem OAI.Problem336.relabelEdgeSet_symm line 52
  10. theorem OAI.Problem336.relabelEdgeSet_valid line 64
  11. theorem OAI.Problem336.treeAdj_relabelEdgeSet line 72
  12. theorem OAI.Problem336.treeOn_relabel line 87
  13. theorem OAI.Problem336.relabelFiniteSubgraph_symm line 106
  14. theorem OAI.Problem336.treeOn_relabel_iff line 113
  15. theorem OAI.Problem336.treeOn_of_mem_spanningTrees line 124
  16. theorem OAI.Problem336.mem_spanningTrees_of_treeOn line 129
  17. theorem OAI.Problem336.spanningTrees_relabel line 134
  18. theorem OAI.Problem336.relabelEdgeSet_injOn_spanningTrees line 153
  19. theorem OAI.Problem336.spanningTrees_card_relabel line 164
  20. theorem OAI.Problem336.mem_relabelEdgeSet_iff line 170
  21. theorem OAI.Problem336.ustCylinder_relabel line 176
  22. theorem OAI.Problem336.IsFiniteConnectedSubgraph.relabel line 220
  23. theorem OAI.Problem336.IsFiniteConnectedSubgraph.ustCylinder_relabel line 254
  24. theorem OAI.Problem336.IsConnectedExhaustion.relabel line 261
  25. theorem OAI.Problem336.HasFUSFLaw.relabel line 287