OAI/Probability/SpanningForest/GraphBorel.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem336.GraphBorel.FiniteReach line 11
  2. theorem OAI.Problem336.GraphBorel.finiteReach_reflTransGen line 15
  3. theorem OAI.Problem336.GraphBorel.reflTransGen_iff_exists_finiteReach line 26
  4. theorem OAI.Problem336.GraphBorel.measurable_finiteReach line 38
  5. theorem OAI.Problem336.GraphBorel.measurable_reflTransGen line 46
  6. theorem OAI.Problem336.GraphBorel.measurable_adj line 52
  7. theorem OAI.Problem336.GraphBorel.measurable_graphConnected line 60
  8. theorem OAI.Problem336.GraphBorel.measurableSet_graphConnected line 64
  9. theorem OAI.Problem336.GraphBorel.finite_setOf_iff line 67
  10. theorem OAI.Problem336.GraphBorel.measurable_finite_setOf line 76
  11. theorem OAI.Problem336.GraphBorel.measurable_graphLocallyFinite line 83
  12. theorem OAI.Problem336.GraphBorel.measurableSet_graphLocallyFinite line 86
  13. theorem OAI.Problem336.GraphBorel.measurableSet_graphSupported line 90
  14. theorem OAI.Problem336.GraphBorel.measurable_isFiniteConnectedSubgraph line 94
  15. theorem OAI.Problem336.GraphBorel.measurable_isConnectedExhaustion line 100
  16. theorem OAI.Problem336.GraphBorel.measurable_injective_labels line 106
  17. theorem OAI.Problem336.GraphBorel.measurableSet_injective_labels line 111