OAI/Probability/SpanningForest/FiniteIncidenceBridge.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem336.FiniteIncidence.ValidEdges line 10
  2. def OAI.Problem336.FiniteIncidence.src line 13
  3. def OAI.Problem336.FiniteIncidence.dst line 16
  4. theorem OAI.Problem336.FiniteIncidence.ValidEdges.mono line 19
  5. def OAI.Problem336.FiniteIncidence.edgeInclusion line 23
  6. theorem OAI.Problem336.FiniteIncidence.reducedGradient_submatrix line 27
  7. theorem OAI.Problem336.FiniteIncidence.edgeAdj_iff_treeAdj line 34
  8. theorem OAI.Problem336.FiniteIncidence.treeAdj_endpoints_mem line 62
  9. theorem OAI.Problem336.FiniteIncidence.treePath_endpoint_mem line 70
  10. theorem OAI.Problem336.FiniteIncidence.treePath_lift line 77
  11. theorem OAI.Problem336.FiniteIncidence.connected_iff_treePaths line 88
  12. theorem OAI.Problem336.FiniteIncidence.validEdges_of_subgraph line 100
  13. theorem OAI.Problem336.FiniteIncidence.treeOn_iff_connected line 107
  14. theorem OAI.Problem336.FiniteIncidence.treeOn_weightedLaplacian_posDef line 116
  15. def OAI.Problem336.FiniteIncidence.edgeEquivNonroot line 125
  16. def OAI.Problem336.FiniteIncidence.treeEdgeEquivNonroot line 132
  17. def OAI.Problem336.FiniteIncidence.squareReducedGradient line 136
  18. theorem OAI.Problem336.FiniteIncidence.squareReducedGradient_det_ne_zero line 141
  19. theorem OAI.Problem336.FiniteIncidence.treeOn_squareReducedGradient_det_ne_zero line 155