OAI/Probability/SpanningForest/GraphBalls.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem336.withinRadius line 11
2. theorem OAI.Problem336.withinRadius_zero line 16
3. theorem OAI.Problem336.withinRadius_succ line 19
4. theorem OAI.Problem336.withinRadius_mono line 23
5. theorem OAI.Problem336.withinRadius_refl line 29
6. theorem OAI.Problem336.withinRadius_reachable line 33
7. theorem OAI.Problem336.exists_withinRadius_of_reachable line 43
8. theorem OAI.Problem336.reachable_iff_exists_withinRadius line 52
9. theorem OAI.Problem336.exists_withinRadius line 56
10. theorem OAI.Problem336.finite_withinRadius line 60
11. theorem OAI.Problem336.measurableSet_adj line 70
12. theorem OAI.Problem336.measurableSet_withinRadius line 76
13. theorem OAI.Problem336.withinRadius_relabel line 86
14. def OAI.Problem336.edgeBall line 105
15. theorem OAI.Problem336.finite_edgeBall line 108
16. theorem OAI.Problem336.edgeBall_mono line 113
17. theorem OAI.Problem336.measurableSet_mem_edgeBall line 118
18. theorem OAI.Problem336.mem_edgeBall_mkEdge line 123
19. theorem OAI.Problem336.mem_edgeBall_mapEdge line 129
20. theorem OAI.Problem336.edgeBall_relabel line 137
21. theorem OAI.Problem336.exists_mem_edgeBall line 148
22. theorem OAI.Problem336.measurable_edgeBall line 153
23. theorem OAI.Problem336.measurable_edgeBall_joint line 158
24. def OAI.Problem336.finiteSetCode line 162
25. theorem OAI.Problem336.finiteSetCode_of_finite line 166
26. theorem OAI.Problem336.finiteSetCode_eq_iff line 170
27. theorem OAI.Problem336.measurable_finiteSetCode line 180
28. def OAI.Problem336.edgeBallCode line 188
29. theorem OAI.Problem336.measurable_edgeBallCode line 191
30. theorem OAI.Problem336.mem_edgeBallCode line 195
31. theorem OAI.Problem336.finiteSetCode_image line 199
32. theorem OAI.Problem336.edgeBallCode_relabel line 209