OAI/Probability/CriticalPercolation/Clusters/ComponentSelf.lean
9 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.CriticalPercolation.ClusterDeletion.component_selfline 15 - lemma
OAI.CriticalPercolation.ClusterDeletion.mem_component_symmline 18 - lemma
OAI.CriticalPercolation.ClusterDeletion.roots_singletonline 22 - lemma
OAI.CriticalPercolation.ClusterDeletion.component_eq_of_memline 26 - lemma
OAI.CriticalPercolation.ClusterDeletion.not_mem_roots_iff_disjointline 31 - lemma
OAI.CriticalPercolation.ClusterDeletion.component_delete_componentline 40 - lemma
OAI.CriticalPercolation.ClusterDeletion.roots_delete_componentline 46 - lemma
OAI.CriticalPercolation.ClusterDeletion.delete_emptyline 59 - lemma
OAI.CriticalPercolation.ClusterDeletion.component_delete_selfline 63