OAI/Probability/CriticalPercolation/GraphGeometry/StripCompactness.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CriticalPercolation.BondGraph.seedDomainTail line 19
2. def OAI.CriticalPercolation.BondGraph.seedDomainInfinite line 22
3. lemma OAI.CriticalPercolation.BondGraph.seedDomainTail_measurable line 25
4. lemma OAI.CriticalPercolation.BondGraph.seedDomainTail_antitone line 32
5. lemma OAI.CriticalPercolation.BondGraph.seedDomainInfinite_eq_iInter line 37
6. lemma OAI.CriticalPercolation.BondGraph.seedDomainInfinite_probability line 58
7. lemma OAI.CriticalPercolation.BondGraph.RayPrefix.reachable line 69
8. lemma OAI.CriticalPercolation.BondGraph.RayPrefix.clusterTail line 83
9. lemma OAI.CriticalPercolation.BondGraph.exit_gives_prefix line 90
10. def OAI.CriticalPercolation.BondGraph.prefix_inside_domain line 120
11. theorem OAI.CriticalPercolation.BondGraph.local_domain_exit_compactness line 127