OAI/Probability/CriticalPercolation/GraphGeometry/FullOrbitalStructureTransfer.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CriticalPercolation.StructurePullback.nilpotent_comap_of_injective line 20
2. lemma OAI.CriticalPercolation.StructurePullback.finiteIndex_comap line 34
3. lemma OAI.CriticalPercolation.BondGraph.finite_stabilizer_images_from_one_vertex line 44
4. def OAI.CriticalPercolation.BondGraph.fullOrbitalQuotientHom line 74
5. lemma OAI.CriticalPercolation.BondGraph.fullOrbital_finite_kernel_orbits line 79
6. lemma OAI.CriticalPercolation.BondGraph.fullOrbital_finite_stabilizer_images line 94
7. theorem OAI.CriticalPercolation.BondGraph.critical_null_of_compact_open_orbital_quotient line 112