OAI/Probability/CriticalPercolation/GraphGeometry/InfiniteEventSubsetHit.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CriticalPercolation.BondGraph.infiniteEvent_subset_hit_compl line 21
2. lemma OAI.CriticalPercolation.BondGraph.infiniteEvent_eq_iInter_hit_compl line 26
3. lemma OAI.CriticalPercolation.BondGraph.tendsto_real_hit_compl line 40
4. lemma OAI.CriticalPercolation.BondGraph.real_hit_singleton_pos line 52
5. lemma OAI.CriticalPercolation.BondGraph.real_infiniteEvent_transfer line 65
6. lemma OAI.CriticalPercolation.BondGraph.real_infiniteEvent_pos_all line 81
7. theorem OAI.CriticalPercolation.BondGraph.uniform_rooted_probability line 88