OAI/Probability/CriticalPercolation/Modular/ActionOrbitTransport.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.ActionOrbitTransport.Representatives line 13
  2. lemma OAI.ActionOrbitTransport.finite_orbits line 18
  3. def OAI.ActionOrbitTransport.representatives line 31
  4. abbrev OAI.ActionOrbitTransport.PairOrbit line 50
  5. def OAI.ActionOrbitTransport.pairOrbit line 51
  6. def OAI.ActionOrbitTransport.stabilizerOrbit line 52
  7. def OAI.ActionOrbitTransport.suborbitCard line 53
  8. lemma OAI.ActionOrbitTransport.mem_stabilizerOrbit line 55
  9. lemma OAI.ActionOrbitTransport.pairOrbit_eq line 64
  10. lemma OAI.ActionOrbitTransport.smul_pairOrbit line 75
  11. lemma OAI.ActionOrbitTransport.smul_suborbitCard line 79
  12. def OAI.ActionOrbitTransport.swapFn line 101
  13. def OAI.ActionOrbitTransport.swapPairOrbit line 107
  14. abbrev OAI.ActionOrbitTransport.Representatives.RootedPair line 115
  15. def OAI.ActionOrbitTransport.Representatives.pairMap line 116
  16. lemma OAI.ActionOrbitTransport.Representatives.fiber_root_eq line 118
  17. lemma OAI.ActionOrbitTransport.Representatives.fiber_snd_mem line 124
  18. def OAI.ActionOrbitTransport.Representatives.fiberEquiv line 130