OAI/Probability/SpanningForest/IntrinsicExhaustion.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem336.IntrinsicExhaustion.vertexBall line 10
  2. theorem OAI.Problem336.IntrinsicExhaustion.mem_vertexBall_zero line 14
  3. theorem OAI.Problem336.IntrinsicExhaustion.mem_vertexBall_succ line 17
  4. theorem OAI.Problem336.IntrinsicExhaustion.vertexBall_mono line 21
  5. theorem OAI.Problem336.IntrinsicExhaustion.center_mem_vertexBall line 24
  6. theorem OAI.Problem336.IntrinsicExhaustion.finite_vertexBall line 28
  7. theorem OAI.Problem336.IntrinsicExhaustion.exists_mem_vertexBall_of_reachable line 38
  8. theorem OAI.Problem336.IntrinsicExhaustion.GraphConnected.exists_mem_vertexBall line 47
  9. theorem OAI.Problem336.IntrinsicExhaustion.mem_vertexBall_relabel line 52
  10. theorem OAI.Problem336.IntrinsicExhaustion.measurableSet_ballAdj line 70
  11. theorem OAI.Problem336.IntrinsicExhaustion.measurableSet_mem_vertexBall line 76
  12. def OAI.Problem336.IntrinsicExhaustion.edgeBall line 84
  13. theorem OAI.Problem336.IntrinsicExhaustion.edgeBall_mono line 87
  14. theorem OAI.Problem336.IntrinsicExhaustion.finite_edgeBall line 92
  15. theorem OAI.Problem336.IntrinsicExhaustion.fst_mem_edgeBall line 96
  16. theorem OAI.Problem336.IntrinsicExhaustion.snd_mem_edgeBall line 99
  17. theorem OAI.Problem336.IntrinsicExhaustion.GraphConnected.exists_mem_edgeBall line 102
  18. theorem OAI.Problem336.IntrinsicExhaustion.mem_edgeBall_relabel line 108
  19. theorem OAI.Problem336.IntrinsicExhaustion.measurableSet_mem_edgeBall line 114
  20. theorem OAI.Problem336.IntrinsicExhaustion.vertexBall_reachable line 119
  21. theorem OAI.Problem336.IntrinsicExhaustion.edgeBall_reachable line 140
  22. def OAI.Problem336.IntrinsicExhaustion.ballInducedSubgraph line 152
  23. theorem OAI.Problem336.IntrinsicExhaustion.ballInducedSubgraph_vertices line 156
  24. theorem OAI.Problem336.IntrinsicExhaustion.mem_ballInducedSubgraph_edges line 159
  25. theorem OAI.Problem336.IntrinsicExhaustion.ballAdj_symm line 166
  26. theorem OAI.Problem336.IntrinsicExhaustion.ballAdj_ne line 169
  27. theorem OAI.Problem336.IntrinsicExhaustion.rawPair_mem_ballInducedSubgraph line 174
  28. theorem OAI.Problem336.IntrinsicExhaustion.subgraphAdj_ballInducedSubgraph line 187
  29. def OAI.Problem336.IntrinsicExhaustion.edgeBallSubgraph line 193
  30. theorem OAI.Problem336.IntrinsicExhaustion.mem_edgeBallSubgraph_vertices line 197
  31. theorem OAI.Problem336.IntrinsicExhaustion.subgraphAdj_edgeBallSubgraph line 202
  32. theorem OAI.Problem336.IntrinsicExhaustion.isFiniteConnectedSubgraph_edgeBallSubgraph line 208
  33. theorem OAI.Problem336.IntrinsicExhaustion.mem_edgeBallSubgraph_edges line 225
  34. theorem OAI.Problem336.IntrinsicExhaustion.isConnectedExhaustion_edgeBallSubgraph line 231
  35. theorem OAI.Problem336.IntrinsicExhaustion.measurable_finset_from_membership line 253
  36. theorem OAI.Problem336.IntrinsicExhaustion.measurable_edgeBallSubgraph line 269