OAI/Probability/SpanningForest/GraphEncoding.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Problem336.FiniteEncoding.rawPair_comm line 9
  2. def OAI.Problem336.FiniteEncoding.graph line 13
  3. lemma OAI.Problem336.FiniteEncoding.rawPair_self line 22
  4. lemma OAI.Problem336.FiniteEncoding.rawPair_ne_of_mem line 24
  5. lemma OAI.Problem336.FiniteEncoding.reachable_of_subgraphPath line 32
  6. lemma OAI.Problem336.FiniteEncoding.connected line 43
  7. def OAI.Problem336.FiniteEncoding.edgePair line 50
  8. lemma OAI.Problem336.FiniteEncoding.edgePair_mk line 53
  9. lemma OAI.Problem336.FiniteEncoding.edgePair_forget line 56
  10. lemma OAI.Problem336.FiniteEncoding.edgePair_injective line 66
  11. def OAI.Problem336.FiniteEncoding.edgePairs line 72
  12. lemma OAI.Problem336.FiniteEncoding.card_edgePairs line 77
  13. lemma OAI.Problem336.FiniteEncoding.rawPair_mem_edgePairs line 83
  14. lemma OAI.Problem336.FiniteEncoding.edgePairs_subset line 89
  15. lemma OAI.Problem336.FiniteEncoding.treeOn_edgePairs line 100
  16. lemma OAI.Problem336.FiniteEncoding.rawPair_mem_endpoints line 112
  17. lemma OAI.Problem336.FiniteEncoding.edgePairs_graph line 121
  18. lemma OAI.Problem336.FiniteEncoding.finiteConnected_treeCode line 134
  19. lemma OAI.Problem336.FiniteEncoding.isTree_graph_treeCode line 147
  20. lemma OAI.Problem336.FiniteEncoding.rawPair_mem_edgePairs_iff line 156
  21. lemma OAI.Problem336.FiniteEncoding.graph_edgePairs line 168
  22. lemma OAI.Problem336.FiniteEncoding.edgePairs_graph_of_valid line 175
  23. lemma OAI.Problem336.FiniteEncoding.treeOn_iff_isTree line 189
  24. lemma OAI.Problem336.FiniteEncoding.mem_spanningTrees_iff line 206
  25. def OAI.Problem336.FiniteEncoding.spanningTreeEquiv line 212
  26. lemma OAI.Problem336.FiniteEncoding.card_spanningTrees line 232
  27. lemma OAI.Problem336.FiniteEncoding.spanningTrees_nonempty line 238