OAI/Probability/CriticalPercolation/Modular/FiniteClusterTransport.lean
8 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.CriticalPercolation.finite_subset_size_imageline 16 - lemma
OAI.CriticalPercolation.BondGraph.induce_clusterTailline 35 - lemma
OAI.CriticalPercolation.BondGraph.induce_twoClusterEventline 42 - lemma
OAI.CriticalPercolation.BondGraph.restrictVertices_cluster_imageline 48 - lemma
OAI.CriticalPercolation.BondGraph.restrictVertices_clusterTailline 59 - lemma
OAI.CriticalPercolation.BondGraph.restrictVertices_twoClusterEventline 66 - lemma
OAI.CriticalPercolation.BondGraph.induce_law_eventline 72 - lemma
OAI.CriticalPercolation.BondGraph.induce_twoCluster_realline 79