OAI/Probability/CriticalPercolation/GraphGeometry/FiniteInduced.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CriticalPercolation.BondGraph.inducedEdges line 15
2. def OAI.CriticalPercolation.BondGraph.induce line 17
3. lemma OAI.CriticalPercolation.BondGraph.induce_ends_map line 20
4. lemma OAI.CriticalPercolation.BondGraph.induce_ends_eq line 24
5. lemma OAI.CriticalPercolation.BondGraph.finite_incident line 29
6. lemma OAI.CriticalPercolation.BondGraph.finite_inducedEdges line 36
7. lemma OAI.CriticalPercolation.BondGraph.induce_adj line 44
8. lemma OAI.CriticalPercolation.BondGraph.induced_adj_mem line 56
9. lemma OAI.CriticalPercolation.BondGraph.induce_reachable line 63
10. lemma OAI.CriticalPercolation.BondGraph.induced_cluster_subset line 82
11. lemma OAI.CriticalPercolation.BondGraph.induce_cluster_image line 90