OAI/Probability/SpanningForest/EdgeBallExhaustion.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem336.fst_mem_edgeBall line 9
  2. theorem OAI.Problem336.snd_mem_edgeBall line 12
  3. theorem OAI.Problem336.withinRadius_reachable_inside line 15
  4. theorem OAI.Problem336.edgeBall_reachable line 36
  5. def OAI.Problem336.ballInducedSubgraph line 48
  6. theorem OAI.Problem336.ballInducedSubgraph_vertices line 52
  7. theorem OAI.Problem336.mem_ballInducedSubgraph_edges line 55
  8. theorem OAI.Problem336.ballAdj_symm line 62
  9. theorem OAI.Problem336.ballAdj_ne line 65
  10. theorem OAI.Problem336.rawPair_mem_ballInducedSubgraph line 70
  11. theorem OAI.Problem336.subgraphAdj_ballInducedSubgraph line 83
  12. def OAI.Problem336.edgeBallSubgraph line 89
  13. theorem OAI.Problem336.mem_edgeBallSubgraph_vertices line 93
  14. theorem OAI.Problem336.subgraphAdj_edgeBallSubgraph line 98
  15. theorem OAI.Problem336.isFiniteConnectedSubgraph_edgeBallSubgraph line 104
  16. theorem OAI.Problem336.mem_edgeBallSubgraph_edges line 121
  17. theorem OAI.Problem336.isConnectedExhaustion_edgeBallSubgraph line 127
  18. theorem OAI.Problem336.measurable_finset_from_membership line 149
  19. theorem OAI.Problem336.measurable_edgeBallSubgraph line 165