OAI/Probability/SpanningForest/Exhaustion.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem336.GraphConnected.exists_adj line 11
2. theorem OAI.Problem336.IsConnectedExhaustion.monotone_vertices line 21
3. theorem OAI.Problem336.IsConnectedExhaustion.monotone_edges line 25
4. theorem OAI.Problem336.IsConnectedExhaustion.eventually_mem_edges line 29
5. theorem OAI.Problem336.IsConnectedExhaustion.eventually_mem_edges_finset line 36
6. theorem OAI.Problem336.IsConnectedExhaustion.endpoints_mem line 43
7. theorem OAI.Problem336.IsConnectedExhaustion.eventually_mem_rawPair line 48
8. theorem OAI.Problem336.IsConnectedExhaustion.eventually_mem_vertices line 66
9. theorem OAI.Problem336.IsConnectedExhaustion.eventually_subset_vertices line 77
10. theorem OAI.Problem336.IsConnectedExhaustion.eventually_subset_edges line 85
11. theorem OAI.Problem336.IsConnectedExhaustion.eventually_contains line 94