OAI/Probability/SpanningForest/AlgebraicCycleSpace.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Problem336.EdgeFlow line 9
  2. def OAI.Problem336.edgeBoundary line 11
  3. theorem OAI.Problem336.edgeBoundary_single line 15
  4. def OAI.Problem336.finiteCodeEdges line 20
  5. def OAI.Problem336.graphCodeEdges line 23
  6. def OAI.Problem336.finiteCycleSpace line 26
  7. def OAI.Problem336.graphCycleSpace line 29
  8. theorem OAI.Problem336.mem_finiteCycleSpace line 32
  9. theorem OAI.Problem336.mem_graphCycleSpace line 37
  10. theorem OAI.Problem336.finiteCycleSpace_mono line 42
  11. theorem OAI.Problem336.IsFiniteConnectedSubgraph.finiteCycleSpace_le line 47
  12. theorem OAI.Problem336.IsConnectedExhaustion.finiteCodeEdges_monotone line 53
  13. theorem OAI.Problem336.IsConnectedExhaustion.iUnion_finiteCodeEdges line 60
  14. theorem OAI.Problem336.IsConnectedExhaustion.finiteCycleSpace_monotone line 72
  15. theorem OAI.Problem336.IsConnectedExhaustion.iSup_finiteCycleSpace line 79
  16. theorem OAI.Problem336.finiteCodeEdges_finite line 88
  17. instance OAI.Problem336.finiteDimensional_finiteCycleSpace line 92
  18. abbrev OAI.Problem336.EdgeHilbert line 100
  19. def OAI.Problem336.edgeFlowToHilbert line 102
  20. theorem OAI.Problem336.edgeFlowToHilbert_single line 105
  21. theorem OAI.Problem336.edgeFlowToHilbert_apply line 109
  22. theorem OAI.Problem336.edgeFlowToHilbert_injective line 119
  23. def OAI.Problem336.finiteHilbertCycleSpace line 124
  24. def OAI.Problem336.closedGraphCycleSpace line 127
  25. instance OAI.Problem336.finiteDimensional_finiteHilbertCycleSpace line 130
  26. theorem OAI.Problem336.finiteHilbertCycleSpace_closed line 135
  27. theorem OAI.Problem336.IsConnectedExhaustion.finiteHilbertCycleSpace_monotone line 139
  28. theorem OAI.Problem336.IsConnectedExhaustion.closure_iSup_finiteHilbertCycleSpace line 145