OAI/Probability/LatticeSurface/Coercivity/BadClusters.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SparseHoles.badCluster line 19
2. def OAI.SparseHoles.badClusters line 24
3. lemma OAI.SparseHoles.mem_badCluster line 28
4. lemma OAI.SparseHoles.badCluster_self line 38
5. lemma OAI.SparseHoles.badCluster_subset line 41
6. lemma OAI.SparseHoles.badCluster_connected line 45
7. lemma OAI.SparseHoles.badCluster_eq_of_reachable line 65
8. lemma OAI.SparseHoles.badClusters_family line 72