OAI/Probability/UnimodularPercolation/Subdivision/Graph.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Subdivision of indexed bond graphs and its basic geometry.

  1. abbrev OAI.Percolation.SubdivisionEdge line 19
  2. def OAI.Percolation.subdivision line 21
  3. theorem OAI.Percolation.subdivision_injective line 24
  4. theorem OAI.Percolation.subdivision_adj_inl_inr line 33
  5. theorem OAI.Percolation.subdivision_adj_inl_inl line 46
  6. theorem OAI.Percolation.subdivision_adj_inr_inr line 51
  7. theorem OAI.Percolation.subdivision_adj_inr_inl line 56
  8. theorem OAI.Percolation.subdivision_loopless line 61
  9. theorem OAI.Percolation.subdivision_locallyFinite line 64
  10. theorem OAI.Percolation.subdivision_connected line 94
  11. theorem OAI.Percolation.incidence_aut_iff line 120
  12. def OAI.Percolation.subdivisionAutEdges line 126
  13. theorem OAI.Percolation.subdivision_isAut line 130
  14. theorem OAI.Percolation.finite_edge_roots line 138
  15. theorem OAI.Percolation.subdivision_quasiTransitive line 152
  16. theorem OAI.Percolation.subdivision_old_boundary_bound line 173
  17. theorem OAI.Percolation.subdivision_new_card_bound line 220
  18. theorem OAI.Percolation.subdivision_hV_pos line 255