OAI/Probability/UnimodularPercolation/Graph/FullTopology.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

The automorphism group with its topology of pointwise convergence.

  1. def OAI.Percolation.graphAutSubgroup line 16
  2. def OAI.Percolation.GraphAut line 26
  3. instance OAI.Percolation.(instance at line 28) line 28
  4. instance OAI.Percolation.(instance at line 31) line 31
  5. def OAI.Percolation.graphAutPerm line 34
  6. theorem OAI.Percolation.graphAutPerm_mem line 37
  7. theorem OAI.Percolation.mem_vertexAut_iff_adj line 40
  8. def OAI.Percolation.autCoordinates line 72
  9. instance OAI.Percolation.graphAutTopology line 75
  10. theorem OAI.Percolation.inducing_autCoordinates line 79
  11. theorem OAI.Percolation.embedding_autCoordinates line 83
  12. instance OAI.Percolation.graphAutT2 line 92
  13. theorem OAI.Percolation.continuous_aut_apply line 96
  14. theorem OAI.Percolation.continuous_aut_inv_apply line 101
  15. theorem OAI.Percolation.continuous_discrete_eval line 105
  16. instance OAI.Percolation.graphAutTopologicalGroup line 108
  17. def OAI.Percolation.autCoordinateSet line 127
  18. theorem OAI.Percolation.range_autCoordinates line 132
  19. theorem OAI.Percolation.continuous_coordinate_forward_inverse line 147
  20. theorem OAI.Percolation.continuous_coordinate_inverse_forward line 154
  21. theorem OAI.Percolation.isClosed_coordinate_forward_inverse line 161
  22. theorem OAI.Percolation.isClosed_coordinate_inverse_forward line 169
  23. theorem OAI.Percolation.isClosed_coordinate_adjacency line 177
  24. theorem OAI.Percolation.isClosed_autCoordinateSet line 192
  25. def OAI.Percolation.graphStabilizer line 197
  26. theorem OAI.Percolation.isOpen_graphStabilizer line 200
  27. theorem OAI.Percolation.isClosed_stabilizer_coordinates line 204
  28. theorem OAI.Percolation.isCompact_graphStabilizer line 223
  29. theorem OAI.Percolation.locallyCompact_graphAut line 242
  30. theorem OAI.Percolation.graphAutTopology_eq_pointwise line 248
  31. instance OAI.Percolation.fullGraphAutSecondCountable line 272
  32. abbrev OAI.Percolation.GraphOrbit line 278
  33. theorem OAI.Percolation.finite_graphOrbit line 280
  34. def OAI.Percolation.fullGraphOrbitRoot line 295
  35. theorem OAI.Percolation.graphOrbitRoot_covers line 297
  36. theorem OAI.Percolation.graphOrbitRoot_separates line 302