OAI/Probability/CriticalPercolation/GraphGeometry/OpenGraphIso.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CriticalPercolation.BernoulliProduct.measurable_image_equiv line 21
2. lemma OAI.CriticalPercolation.BernoulliProduct.law_map_equiv line 30
3. lemma OAI.CriticalPercolation.BernoulliProduct.real_law_subset line 42
4. instance OAI.CriticalPercolation.BondGraph.law_probability line 61
5. lemma OAI.CriticalPercolation.BondGraph.Aut.adj_map line 65
6. def OAI.CriticalPercolation.BondGraph.Aut.openGraphIso line 79
7. lemma OAI.CriticalPercolation.BondGraph.Aut.cluster_image line 84
8. def OAI.CriticalPercolation.BondGraph.infiniteEvent line 93
9. lemma OAI.CriticalPercolation.BondGraph.measurableSet_infiniteEvent line 95
10. lemma OAI.CriticalPercolation.BondGraph.Aut.preimage_infiniteEvent line 98
11. lemma OAI.CriticalPercolation.BondGraph.law_map_aut line 106
12. lemma OAI.CriticalPercolation.BondGraph.Aut.infiniteEvent_measure line 111
13. lemma OAI.CriticalPercolation.BondGraph.Aut.infiniteEvent_real line 118