OAI/Probability/SpanningForest/DisconnectedIncidence.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem336.IncidenceDisconnected.EndpointAdj line 13
2. theorem OAI.Problem336.IncidenceDisconnected.reachable_endpoints_iff line 16
3. def OAI.Problem336.IncidenceDisconnected.reducedIncidence line 27
4. theorem OAI.Problem336.IncidenceDisconnected.sum_reduced_indicator line 31
5. theorem OAI.Problem336.IncidenceDisconnected.vecMul_reducedIncidence line 44
6. theorem OAI.Problem336.IncidenceDisconnected.exists_nonzero_vecMul_reducedIncidence_eq_zero line 52
7. theorem OAI.Problem336.IncidenceDisconnected.det_reducedIncidence_eq_zero_of_not_connected line 73
8. theorem OAI.Problem336.IncidenceDisconnected.det_reindexed_reducedIncidence_eq_zero_of_not_connected line 80
9. theorem OAI.Problem336.IncidenceDisconnected.det_reducedLaplacian_eq_zero_of_not_connected line 90
10. theorem OAI.Problem336.IncidenceDisconnected.connected_of_det_reducedIncidence_ne_zero line 100