OAI/Probability/SpanningForest/IntrinsicBridge.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem336.Intrinsic.withinRadius_iff_vertexBall line 13
2. theorem OAI.Problem336.Intrinsic.edgeBall_eq_selected line 20
3. def OAI.Problem336.Intrinsic.exhaustion line 26
4. theorem OAI.Problem336.Intrinsic.measurable_exhaustion line 29
5. theorem OAI.Problem336.Intrinsic.exhaustion_eq_edgeBallSubgraph line 33
6. theorem OAI.Problem336.Intrinsic.subgraphAdj_exhaustion line 44
7. theorem OAI.Problem336.Intrinsic.exhaustion_finiteConnected line 50
8. theorem OAI.Problem336.Intrinsic.exhaustion_mono line 56
9. theorem OAI.Problem336.Intrinsic.isConnectedExhaustion line 65