OAI/Probability/CriticalPercolation/GraphGeometry/OrbitalStructureTransfer.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.CriticalPercolation.BondGraph.orbitalActionGroup_action line 18
2. def OAI.CriticalPercolation.BondGraph.orbitalQuotientMap line 24
3. lemma OAI.CriticalPercolation.BondGraph.orbitalQuotientMap_surjective line 29
4. lemma OAI.CriticalPercolation.BondGraph.orbitalQuotientMap_finite_kernel_orbits line 34
5. def OAI.CriticalPercolation.BondGraph.orbitalBlockProjection line 51
6. lemma OAI.CriticalPercolation.BondGraph.orbitalBlockProjection_equivariant line 57
7. lemma OAI.CriticalPercolation.BondGraph.orbitalQuotientMap_finite_stabilizer_images line 68
8. theorem OAI.CriticalPercolation.BondGraph.critical_null_of_orbital_nilpotent_quotient line 82