OAI/Probability/UnimodularPercolation/Graph/Topology.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Pointwise topology on permutation groups.

  1. def OAI.Percolation.PointwisePerm.coordinates line 17
  2. instance OAI.Percolation.PointwisePerm.topology line 19
  3. theorem OAI.Percolation.PointwisePerm.isEmbedding_coordinates line 23
  4. theorem OAI.Percolation.PointwisePerm.continuous_apply line 29
  5. theorem OAI.Percolation.PointwisePerm.continuous_symm_apply line 33
  6. theorem OAI.Percolation.PointwisePerm.continuous_eval line 36
  7. instance OAI.Percolation.PointwisePerm.topologicalGroup line 39
  8. instance OAI.Percolation.PointwisePerm.hausdorff line 58
  9. instance OAI.Percolation.PointwisePerm.secondCountable line 61
  10. theorem OAI.Percolation.PointwisePerm.topology_eq_pointwise line 66
  11. theorem OAI.Percolation.PointwisePerm.range_coordinates line 93
  12. theorem OAI.Percolation.PointwisePerm.isClosed_range_coordinates line 102
  13. theorem OAI.Percolation.PointwisePerm.isCompact_of_finite_images line 118
  14. theorem OAI.Percolation.PointwisePerm.isOpen_fixed line 131
  15. theorem OAI.Percolation.PointwisePerm.isClosed_fixed line 134