OAI/Probability/CriticalPercolation/GraphTopology/CompactOrbitKernel.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CriticalPercolation.GraphTopology.orbitKernel line 16
2. instance OAI.CriticalPercolation.GraphTopology.orbitKernel_normal line 19
3. lemma OAI.CriticalPercolation.GraphTopology.mem_orbitKernel_iff line 22
4. lemma OAI.CriticalPercolation.GraphTopology.le_orbitKernel line 35
5. lemma OAI.CriticalPercolation.GraphTopology.orbitKernel_closed line 41
6. lemma OAI.CriticalPercolation.GraphTopology.compact_orbitKernel line 50
7. lemma OAI.CriticalPercolation.GraphTopology.open_orbitKernel_of_locallyConnected_quotient line 65
8. theorem OAI.CriticalPercolation.GraphTopology.compact_open_orbitKernel_of_locallyConnected_quotient line 97
9. theorem OAI.CriticalPercolation.GraphTopology.compact_open_orbitKernel_of_open_locallyConnected_subquotient line 105