OAI/Probability/CriticalPercolation/GraphGeometry/NormalOrbitAction.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.CriticalPercolation.NormalOrbit.Blocks line 14
2. def OAI.CriticalPercolation.NormalOrbit.block line 16
3. lemma OAI.CriticalPercolation.NormalOrbit.map_rel line 18
4. def OAI.CriticalPercolation.NormalOrbit.blockPerm line 25
5. lemma OAI.CriticalPercolation.NormalOrbit.blockPerm_block line 37
6. def OAI.CriticalPercolation.NormalOrbit.blockHom line 40
7. lemma OAI.CriticalPercolation.NormalOrbit.le_ker_blockHom line 51
8. def OAI.CriticalPercolation.NormalOrbit.quotientHom line 60
9. instance OAI.CriticalPercolation.NormalOrbit.quotientAction line 63
10. lemma OAI.CriticalPercolation.NormalOrbit.mk_smul_block line 66
11. lemma OAI.CriticalPercolation.NormalOrbit.block_eq_iff line 70
12. lemma OAI.CriticalPercolation.NormalOrbit.quotient_stabilizer_contains_image line 73
13. lemma OAI.CriticalPercolation.NormalOrbit.finite_stabilizer_image line 80